Skip to content

Commit bdf278b

Browse files
tautschnigtautschnig
committed
label_properties: do not rely on source_locationt's get_function()
A source location is a place in a text file, and the function information stored in there need not coincide with the name we use in the goto model. In this vein, label_properties should use the actual function name so that properties in different instantiations of a function (as may happen when linking static functions) get unique names.
1 parent 0a09814 commit bdf278b

File tree

103 files changed

+387
-355
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

103 files changed

+387
-355
lines changed

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException1:()V.1'
3+
--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException2:()V.1'
3+
--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetLength/test_exception.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException:()V.1'
3+
--function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException1:()V.1'
3+
--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException2:()V.1'
3+
--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_exception.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException:()V.1'
3+
--function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc/exceptions28/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
test
33
--unwind 10
4-
^\[java::test.main:\(\[Ljava/lang/String;\)V\.1\] line 7 no uncaught exception: FAILURE$
4+
^\[__CPROVER__start\.1\] line 7 no uncaught exception: FAILURE$
55
^VERIFICATION FAILED$
66
^EXIT=10$
77
^SIGNAL=0$

‎regression/cbmc/link_json_symtabs/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ one.json_symtab
33
two.json_symtab
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[1\] file two.adb line [0-9]+ assertion: SUCCESS
6+
\[two\.1\] file two.adb line [0-9]+ assertion: SUCCESS
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/cbmc/unique_labels1/bar.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
static int foo()
4+
{
5+
assert(1 < 0);
6+
}
7+
8+
void bar()
9+
{
10+
foo();
11+
}

‎regression/cbmc/unique_labels1/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
static int foo()
4+
{
5+
assert(0);
6+
}
7+
8+
void bar();
9+
10+
int main()
11+
{
12+
foo();
13+
bar();
14+
}

0 commit comments

Comments
 (0)