Merge pull request #13 from tautschnig/sv-comp-verifier-atomic

Daniel Kroening · Daniel Kroening · commit 6f4fad0d204a · 2016-03-06T21:22:57.000Z
Support SV-COMP's __VERIFIER_atomic_{begin,end}
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -1201,12 +1201,14 @@ void goto_convertt::do_function_call_symbol(
     do_output(lhs, function, arguments, dest);
   }
   else if(identifier==CPROVER_PREFIX "atomic_begin" ||
-          identifier=="__CPROVER::atomic_begin")
+          identifier=="__CPROVER::atomic_begin" ||
+          identifier=="__VERIFIER_atomic_begin")
   {
     do_atomic_begin(lhs, function, arguments, dest);
   }
   else if(identifier==CPROVER_PREFIX "atomic_end" ||
-          identifier=="__CPROVER::atomic_end")
+          identifier=="__CPROVER::atomic_end" ||
+          identifier=="__VERIFIER_atomic_end")
   {
     do_atomic_end(lhs, function, arguments, dest);
   }

Original file line number	Diff line number	Diff line change
`@@ -1201,12 +1201,14 @@ void goto_convertt::do_function_call_symbol(`
`1201`	`1201`	`do_output(lhs, function, arguments, dest);`
`1202`	`1202`	`}`
`1203`	`1203`	`else if(identifier==CPROVER_PREFIX "atomic_begin" \|\|`
`1204`		`- identifier=="__CPROVER::atomic_begin")`
	`1204`	`+ identifier=="__CPROVER::atomic_begin" \|\|`
	`1205`	`+ identifier=="__VERIFIER_atomic_begin")`
`1205`	`1206`	`{`
`1206`	`1207`	`do_atomic_begin(lhs, function, arguments, dest);`
`1207`	`1208`	`}`
`1208`	`1209`	`else if(identifier==CPROVER_PREFIX "atomic_end" \|\|`
`1209`		`- identifier=="__CPROVER::atomic_end")`
	`1210`	`+ identifier=="__CPROVER::atomic_end" \|\|`
	`1211`	`+ identifier=="__VERIFIER_atomic_end")`
`1210`	`1212`	`{`
`1211`	`1213`	`do_atomic_end(lhs, function, arguments, dest);`
`1212`	`1214`	`}`