Replace assert.h includes with goblint.h (issue #814)

goblint · Oct 4, 2022 · 3ba2cd9 · 3ba2cd9
1 parent 840f4dd
commit 3ba2cd9
Show file tree

Hide file tree

Showing 673 changed files with 644 additions and 676 deletions.
diff --git a/tests/incremental/00-basic/00-local.c b/tests/incremental/00-basic/00-local.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int main() {
     int x = 1;

diff --git a/tests/incremental/00-basic/00-local.patch b/tests/incremental/00-basic/00-local.patch
@@ -1,7 +1,7 @@
 --- tests/incremental/00-basic/00-local.c	2021-09-30 13:12:18.381946503 +0300
 +++ tests/incremental/00-basic/00-local.c	2021-09-30 13:12:32.697729338 +0300
 @@ -1,7 +1,7 @@
- #include <assert.h>
+ #include <goblint.h>
 
  int main() {
 -    int x = 1;

diff --git a/tests/incremental/00-basic/02-changed_start_state1.c b/tests/incremental/00-basic/02-changed_start_state1.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int g = 1;
 

diff --git a/tests/incremental/00-basic/02-changed_start_state1.patch b/tests/incremental/00-basic/02-changed_start_state1.patch
@@ -1,7 +1,7 @@
 --- tests/incremental/00-basic/02-changed_start_state1.c
 +++ tests/incremental/00-basic/02-changed_start_state1.c
 @@ -1,13 +1,13 @@
- #include <assert.h>
+ #include <goblint.h>
 
 -int g = 1;
 +int g = 2;

diff --git a/tests/incremental/00-basic/03-changed_start_state2.c b/tests/incremental/00-basic/03-changed_start_state2.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int g = 1;
 

diff --git a/tests/incremental/00-basic/03-changed_start_state2.patch b/tests/incremental/00-basic/03-changed_start_state2.patch
@@ -1,7 +1,7 @@
 --- tests/incremental/00-basic/03-changed_start_state2.c
 +++ tests/incremental/00-basic/03-changed_start_state2.c
 @@ -1,13 +1,13 @@
- #include <assert.h>
+ #include <goblint.h>
 
 -int g = 1;
 +int g = 2;

diff --git a/tests/incremental/00-basic/05-sideeffects.c b/tests/incremental/00-basic/05-sideeffects.c
@@ -1,5 +1,5 @@
 // The patch for this test case is empty on purpose. The problem described does occur in the incremental run even without any changes.
-#include <assert.h>
+#include <goblint.h>
 
 int g = 1;
 

diff --git a/tests/incremental/00-basic/07-dead-branch.c b/tests/incremental/00-basic/07-dead-branch.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 void foo() {
 

diff --git a/tests/incremental/00-basic/07-dead-branch.patch b/tests/incremental/00-basic/07-dead-branch.patch
@@ -1,7 +1,7 @@
 --- tests/incremental/00-basic/07-dead-branch.c
 +++ tests/incremental/00-basic/07-dead-branch.c
 @@ -1,7 +1,7 @@
- #include <assert.h>
+ #include <goblint.h>
 
  void foo() {
 -

diff --git a/tests/incremental/00-basic/09-unreach.c b/tests/incremental/00-basic/09-unreach.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 void foo() {
   int x = 2;

diff --git a/tests/incremental/00-basic/10-reach.c b/tests/incremental/00-basic/10-reach.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include<pthread.h>
 
 void foo() {

diff --git a/tests/incremental/00-basic/11-unreach-reusesuper.c b/tests/incremental/00-basic/11-unreach-reusesuper.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 void foo() {
   int x = 2;

diff --git a/tests/incremental/01-force-reanalyze/00-int.c b/tests/incremental/01-force-reanalyze/00-int.c
@@ -1,4 +1,4 @@
-#include<assert.h>
+#include <goblint.h>
 
 int f(int in){
   while(in < 17) {

diff --git a/tests/incremental/01-force-reanalyze/01-int-reluctant.c b/tests/incremental/01-force-reanalyze/01-int-reluctant.c
@@ -1,4 +1,4 @@
-#include<assert.h>
+#include <goblint.h>
 
 int f(int in){
   while(in < 17) {

diff --git a/tests/incremental/03-precision-annotation/01-change_precision.c b/tests/incremental/03-precision-annotation/01-change_precision.c
@@ -1,5 +1,5 @@
 //PARAM: --enable annotation.int.enabled
-#include <assert.h>
+#include <goblint.h>
 #include <math.h>
 
 int main() __attribute__ ((goblint_precision("def_exc","interval")));

diff --git a/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c
@@ -1,4 +1,4 @@
-#include<assert.h>
+#include <goblint.h>
 
 int f(int in){
   while(in < 17) {

diff --git a/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.patch b/tests/incremental/03-precision-annotation/02-reluctant-int-annotation.patch
@@ -3,7 +3,7 @@ index 38187f1c0..698e45b62 100644
 --- tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c
 +++ tests/incremental/03-precision-annotation/02-reluctant-int-annotation.c
 @@ -1,10 +1,11 @@
- #include<assert.h>
+ #include <goblint.h>
 
 +int f(int in) __attribute__ ((goblint_precision("def_exc", "interval")));
  int f(int in){

diff --git a/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c b/tests/incremental/03-precision-annotation/03-reluctant-int-annotation-dyn.c
@@ -1,4 +1,4 @@
-#include<assert.h>
+#include <goblint.h>
 
 typedef int int_to_int_fun (int);
 

diff --git a/tests/incremental/04-var-rename/04-renamed_assert.c b/tests/incremental/04-var-rename/04-renamed_assert.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int main() {
     int myVar = 0;

diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.c b/tests/incremental/04-var-rename/multiple_incremental_runs/08-2_incremental_runs_1.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int main() {
     int varFirstIteration = 0;

diff --git a/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.c b/tests/incremental/04-var-rename/multiple_incremental_runs/09-2_ir_with_changes_1.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 void foo() {
     int fooOne = 1;

diff --git a/tests/incremental/11-restart/01-global-nochange.c b/tests/incremental/11-restart/01-global-nochange.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/02-global-remove.c b/tests/incremental/11-restart/02-global-remove.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/03-global-change.c b/tests/incremental/11-restart/03-global-change.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/04-global-add.c b/tests/incremental/11-restart/04-global-add.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/05-local-wpoint.c b/tests/incremental/11-restart/05-local-wpoint.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/06-local-wpoint-read.c b/tests/incremental/11-restart/06-local-wpoint-read.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/07-local-wpoint-nochange.c b/tests/incremental/11-restart/07-local-wpoint-nochange.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/08-side-restart.c b/tests/incremental/11-restart/08-side-restart.c
@@ -1,5 +1,5 @@
 #include <pthread.h>
-#include <assert.h>
+#include <goblint.h>
 
 int g;
 

diff --git a/tests/incremental/11-restart/09-call-remove.c b/tests/incremental/11-restart/09-call-remove.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 int g = 1;

diff --git a/tests/incremental/11-restart/11-paper-example.c b/tests/incremental/11-restart/11-paper-example.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 #include <pthread.h>
 
 pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;

diff --git a/tests/incremental/11-restart/13-changed_start_state2.c b/tests/incremental/11-restart/13-changed_start_state2.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int g = 1;
 

diff --git a/tests/incremental/11-restart/13-changed_start_state2.patch b/tests/incremental/11-restart/13-changed_start_state2.patch
@@ -1,7 +1,7 @@
 --- tests/incremental/11-restart/13-changed_start_state2.c
 +++ tests/incremental/11-restart/13-changed_start_state2.c
 @@ -1,13 +1,13 @@
- #include <assert.h>
+ #include <goblint.h>
 
 -int g = 1;
 +int g = 2;

diff --git a/tests/incremental/11-restart/48-local-wpoint-funcall.c b/tests/incremental/11-restart/48-local-wpoint-funcall.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int f(int x) {
     return 1;

diff --git a/tests/incremental/11-restart/48-local-wpoint-funcall.patch b/tests/incremental/11-restart/48-local-wpoint-funcall.patch
@@ -1,7 +1,7 @@
 --- tests/incremental/11-restart/48-local-wpoint-funcall.c
 +++ tests/incremental/11-restart/48-local-wpoint-funcall.c
 @@ -1,7 +1,7 @@
- #include <assert.h>
+ #include <goblint.h>
 
  int f(int x) {
 -    return 1;

diff --git a/tests/incremental/13-restart-write/04-malloc-node.c b/tests/incremental/13-restart-write/04-malloc-node.c
@@ -1,5 +1,4 @@
 #include <pthread.h>
-#include <assert.h>
 
 void *t_fun(void *arg) {
   int *iarg = (int*) arg;

diff --git a/tests/incremental/13-restart-write/05-race-call-remove.c b/tests/incremental/13-restart-write/05-race-call-remove.c
@@ -1,5 +1,4 @@
 #include <pthread.h>
-#include <assert.h>
 
 int g;
 

diff --git a/tests/incremental/14-manual-restart/01-restart_manual_simple.c b/tests/incremental/14-manual-restart/01-restart_manual_simple.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int g = 4;
 

diff --git a/tests/incremental/14-manual-restart/01-restart_manual_simple.patch b/tests/incremental/14-manual-restart/01-restart_manual_simple.patch
@@ -3,7 +3,7 @@ index cbfb0ba70..aa83393ac 100644
 --- tests/incremental/14-manual-restart/01-restart_manual_simple.c
 +++ tests/incremental/14-manual-restart/01-restart_manual_simple.c
 @@ -1,9 +1,9 @@
- #include <assert.h>
+ #include <goblint.h>
 
 -int g = 4;
 +int g = 5;

diff --git a/tests/incremental/14-manual-restart/03-partial_contexts.c b/tests/incremental/14-manual-restart/03-partial_contexts.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 int foo(int x){
     return x;
 }

diff --git a/tests/regression/00-sanity/04-empty_if.c b/tests/regression/00-sanity/04-empty_if.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int main()
 {

diff --git a/tests/regression/00-sanity/12-errno.c b/tests/regression/00-sanity/12-errno.c
@@ -1,5 +1,5 @@
 #include <errno.h>
-#include <assert.h>
+#include <goblint.h>
 
 int main(){
 	errno = 1;

diff --git a/tests/regression/00-sanity/13-sans_context.c b/tests/regression/00-sanity/13-sans_context.c
@@ -1,5 +1,5 @@
 // PARAM: --set ana.ctx_insens[+] base
-#include <assert.h>
+#include <goblint.h>
 
 void f(int v, int i){
   __goblint_check(v   == 2);

diff --git a/tests/regression/00-sanity/14-startstate.c b/tests/regression/00-sanity/14-startstate.c
@@ -1,5 +1,5 @@
 // PARAM: --set kernel true
-#include <assert.h>
+#include <goblint.h>
 #include <linux/device.h>
 
 int __init start (unsigned count) {

diff --git a/tests/regression/00-sanity/16-unknown_branches.c b/tests/regression/00-sanity/16-unknown_branches.c
@@ -1,5 +1,5 @@
 // Making sure unknown conditions result in evaluating both branches.
-#include<assert.h>
+#include <goblint.h>
 
 extern int * anIntPlease();
 int main() {

diff --git a/tests/regression/00-sanity/17-constructors.c b/tests/regression/00-sanity/17-constructors.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int g=0;
 

diff --git a/tests/regression/00-sanity/19-if-0.c b/tests/regression/00-sanity/19-if-0.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 void stuff() {
 

diff --git a/tests/regression/00-sanity/20-if-0-realnode.c b/tests/regression/00-sanity/20-if-0-realnode.c
@@ -1,5 +1,3 @@
-#include <assert.h>
-
 void stuff() {
 
 }

diff --git a/tests/regression/00-sanity/22-modulo.c b/tests/regression/00-sanity/22-modulo.c
@@ -1,4 +1,4 @@
-#include "assert.h"
+#include <goblint.h>
 int main() {
     int x = -1;
     int m = x % 5;

diff --git a/tests/regression/00-sanity/23-modulo-interval.c b/tests/regression/00-sanity/23-modulo-interval.c
@@ -1,5 +1,5 @@
 // PARAM: --disable ana.int.def_exc --enable ana.int.interval
-#include "assert.h"
+#include <goblint.h>
 int main() {
     int x = -1;
     int m = x % 5;

diff --git a/tests/regression/00-sanity/24-update_suite.c b/tests/regression/00-sanity/24-update_suite.c
@@ -1,5 +1,5 @@
 // SKIP (just for manually testing that update_suite works)
-#include <assert.h>
+#include <goblint.h>
 
 int main() {
   int x = 42;

diff --git a/tests/regression/00-sanity/25-cfg-connect.c b/tests/regression/00-sanity/25-cfg-connect.c
@@ -1,4 +1,4 @@
-#include <assert.h>
+#include <goblint.h>
 
 int main()
 {

diff --git a/tests/regression/00-sanity/26-strict-loop-enter.c b/tests/regression/00-sanity/26-strict-loop-enter.c
@@ -1,5 +1,5 @@
 //PARAM: --disable ana.int.def_exc --enable ana.int.interval --set solver slr3tp
-#include <assert.h>
+#include <goblint.h>
 
 int g = 0;
 

diff --git a/tests/regression/00-sanity/28-strict-multi-entry-loop.c b/tests/regression/00-sanity/28-strict-multi-entry-loop.c
@@ -1,5 +1,5 @@
 // PARAM: --enable dbg.cfg.loop-clusters
-#include <assert.h>
+#include <goblint.h>
 
 int cycle2_1() {
   int r = 1; // variable to prevent CIL simplification

diff --git a/tests/regression/00-sanity/30-both_branches.c b/tests/regression/00-sanity/30-both_branches.c
@@ -1,5 +1,5 @@
 // PARAM: --enable exp.earlyglobs --disable exp.fast_global_inits
-#include <assert.h>
+#include <goblint.h>
 
 union bloirg {
    int iValdue ;

diff --git a/tests/regression/00-sanity/40-wpoint-restart-sound.c b/tests/regression/00-sanity/40-wpoint-restart-sound.c
@@ -1,6 +1,6 @@
 // PARAM: --enable ana.int.interval
 #include <pthread.h>
-#include <assert.h>
+#include <goblint.h>
 
 int g = 0;
 

diff --git a/tests/regression/01-cpa/01-expressions.c b/tests/regression/01-cpa/01-expressions.c
@@ -1,5 +1,5 @@
 #include<stdio.h>
-#include<assert.h>
+#include <goblint.h>
 
 int glob1;
 int glob2 = 9;

diff --git a/tests/regression/01-cpa/02-branch.c b/tests/regression/01-cpa/02-branch.c
@@ -1,5 +1,5 @@
 #include<stdio.h>
-#include<assert.h>
+#include <goblint.h>
 
 int main() {
   int i,j,k;

diff --git a/tests/regression/01-cpa/03-loops.c b/tests/regression/01-cpa/03-loops.c
@@ -1,5 +1,5 @@
 #include<stdio.h>
-#include<assert.h>
+#include <goblint.h>
 
 int main () {
   int i,j,k;