Avoid spurious arithmetic overflow in CBMC proofs (#130)

feliperodri · web-flow · commit a0223a8c2832 · 2022-12-07T08:06:13.000-08:00
* Avoid spurious arithmetic overflow in CBMC proofs
* Ignore macOS artifacts
* Ignore IDE artifacts

Signed-off-by: Felipe R. Monteiro &lt;felisous@amazon.com&gt;
diff --git a/.gitignore b/.gitignore
@@ -11,3 +11,9 @@ build/
 *.gcda
 *.gcno
 *.gcov
+
+# Ignore macOS artifacts
+.DS_Store
+
+# Ignore IDE artifacts
+.vscode/
diff --git a/test/cbmc/stubs/skipGeneric.c b/test/cbmc/stubs/skipGeneric.c
@@ -41,7 +41,8 @@ static bool skipGeneric( const char * buf,
 
     if( *start < max )
     {
-        assert( __CPROVER_r_ok( ( buf + *start ), ( max - *start ) ) );
+        size_t readable_length = max - *start;
+        assert( __CPROVER_r_ok( ( buf + *start ), readable_length ) );
 
         if( nondet_bool() && ( min <= max ) )
         {

Original file line number	Diff line number	Diff line change
`@@ -41,7 +41,8 @@ static bool skipGeneric( const char * buf,`
`41`	`41`
`42`	`42`	`if( *start < max )`
`43`	`43`	`{`
`44`		`- assert( __CPROVER_r_ok( ( buf + start ), ( max - start ) ) );`
	`44`	`+ size_t readable_length = max - *start;`
	`45`	`+ assert( __CPROVER_r_ok( ( buf + *start ), readable_length ) );`
`45`	`46`
`46`	`47`	`if( nondet_bool() && ( min <= max ) )`
`47`	`48`	`{`