File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -26,14 +26,14 @@ int main(){
2626 check (j == 6 ); // assert UNKNOWN
2727
2828 unknown (& k );
29- assume (k == 4 ); // TODO? assert SUCCESS
29+ assume (k == 4 );
3030 check (k == 4 ); // assert SUCCESS
3131
3232 unknown (& k );
33- assume (k + 1 == n ); // TODO? FAIL
33+ assume (k + 1 == n );
3434
35- assume (n == 5 ); // TODO? NOWARN
36- assert (0 ); // NOWARN
35+ assume (n == 5 ); // contradiction
36+ assert (0 ); // NOWARN (unreachable)
3737
3838 return 0 ;
3939}
Original file line number Diff line number Diff line change @@ -17,7 +17,7 @@ int main() {
1717 create_threads (t );
1818 q = p ;
1919 pthread_mutex_lock (& mutex );
20- assert_racefree (* q ); // TODO
20+ assert_racefree (* q );
2121 pthread_mutex_unlock (& mutex );
2222 return 0 ;
2323}
Original file line number Diff line number Diff line change 33
44int further (int n ) {
55 // Even sides-local can not save us here :(
6- __goblint_check (n <= 1 ); //TODO
6+ __goblint_check (n <= 2 ); //TODO
77}
88
99
1010int fun (int n , const char * arg ) {
1111 // Fails with solvers.td3.side_widen sides, needs sides-local
12- __goblint_check (n <= 1 );
12+ __goblint_check (n <= 2 );
1313 further (n );
1414}
1515
@@ -26,5 +26,5 @@ int main() {
2626 doIt ("two" );
2727
2828 // In the setting with solvers.td3.side_widen sides, widening happens and the bound is lost
29- fun (1 , "org" );
29+ fun (2 , "org" );
3030}
You can’t perform that action at this time.
0 commit comments