goblint · michael-schwarz · Apr 17, 2024 · Apr 17, 2024 · Apr 17, 2024 · Apr 17, 2024
diff --git a/.gitignore b/.gitignore
@@ -22,4 +22,7 @@ result/
 cfgs/
 .goblint/
 *.prec
-
+esop23_table2_set_goblint/*
+esop23_table2_set_watts/*
+esop23_table2_set_ratcop/*
+esop23_table2_set_our/*
diff --git a/concrat/AirConnect/main.c → concrat/AirConnect/airConnect.c b/concrat/AirConnect/main.c → concrat/AirConnect/airConnect.c
diff --git a/concrat/C-Thread-Pool/main.c → concrat/C-Thread-Pool/cThreadPool.c b/concrat/C-Thread-Pool/main.c → concrat/C-Thread-Pool/cThreadPool.c
diff --git a/concrat/C-Thread-Pool/cThreadPool_traces_rel.yml b/concrat/C-Thread-Pool/cThreadPool_traces_rel.yml
diff --git a/concrat/Cello/main.c → concrat/Cello/cello.c b/concrat/Cello/main.c → concrat/Cello/cello.c
diff --git a/concrat/Chipmunk2D/main.c → concrat/Chipmunk2D/chipmunk2d.c b/concrat/Chipmunk2D/main.c → concrat/Chipmunk2D/chipmunk2d.c
diff --git a/concrat/EasyLogger/main.c → concrat/EasyLogger/easyLogger.c b/concrat/EasyLogger/main.c → concrat/EasyLogger/easyLogger.c
diff --git a/concrat/EasyLogger/easyLogger_traces_rel.yml b/concrat/EasyLogger/easyLogger_traces_rel.yml
diff --git a/concrat/Mirai-Source-Code-fixed/main.c → ...rat/Mirai-Source-Code-fixed/mirai-fixed.c b/concrat/Mirai-Source-Code-fixed/main.c → ...rat/Mirai-Source-Code-fixed/mirai-fixed.c
diff --git a/concrat/Mirai-Source-Code/main.c → concrat/Mirai-Source-Code/mirai.c b/concrat/Mirai-Source-Code/main.c → concrat/Mirai-Source-Code/mirai.c
diff --git a/concrat/ProcDump-for-Linux/main.c → concrat/ProcDump-for-Linux/procDump.c b/concrat/ProcDump-for-Linux/main.c → concrat/ProcDump-for-Linux/procDump.c
diff --git a/concrat/Remotery/main.c → concrat/Remotery/remotery.c b/concrat/Remotery/main.c → concrat/Remotery/remotery.c
diff --git a/concrat/axel/main.c → concrat/axel/axel.c b/concrat/axel/main.c → concrat/axel/axel.c
diff --git a/concrat/brubeck/main.c → concrat/brubeck/brubeck.c b/concrat/brubeck/main.c → concrat/brubeck/brubeck.c
diff --git a/concrat/brubeck/brubeck_traces_rel.yml b/concrat/brubeck/brubeck_traces_rel.yml
diff --git a/concrat/cava/main.c → concrat/cava/cava.c b/concrat/cava/main.c → concrat/cava/cava.c
diff --git a/concrat/cava/cava_traces_rel.yml b/concrat/cava/cava_traces_rel.yml
diff --git a/concrat/clib/main.c → concrat/clib/clib.c b/concrat/clib/main.c → concrat/clib/clib.c
diff --git a/concrat/dnspod-sr-fixed/main.c → concrat/dnspod-sr-fixed/dnspod-sr-fixed.c b/concrat/dnspod-sr-fixed/main.c → concrat/dnspod-sr-fixed/dnspod-sr-fixed.c
diff --git a/concrat/dnspod-sr/main.c → concrat/dnspod-sr/dnspod-sr.c b/concrat/dnspod-sr/main.c → concrat/dnspod-sr/dnspod-sr.c
diff --git a/concrat/dump1090/main.c → concrat/dump1090/dump1090.c b/concrat/dump1090/main.c → concrat/dump1090/dump1090.c
diff --git a/concrat/dump1090/dump1090_traces_rel.yml b/concrat/dump1090/dump1090_traces_rel.yml
@@ -0,0 +1,62 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 2db75a6e-bfe8-4d64-8ebc-74adde834000
+    creation_time: 2024-08-11T07:43:15Z
+    producer:
+      name: Goblint
+      version: heads/michael-schwarz-dissertation-0-gccca4b23e-dirty
+      command_line: '''../../../analyzer/goblint'' ''--enable'' ''pre.keep'' ''--conf''
+        ''../../../analyzer/conf/traces-rel.json'' ''--set'' ''dbg.timeout'' ''1200''
+        ''--set'' ''ana.activated[+]'' ''threadJoins'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
+        ''witness.yaml.enabled'' ''dump1090.c'' ''--set'' ''witness.yaml.path'' ''dump1090_traces_rel.yml'''
+    task:
+      input_files:
+      - dump1090.c
+      input_file_hashes:
+        dump1090.c: de7cfc1fd2c72b08913bcac34637a8b24879904453d16ab46e2112fb034fb637
+      data_model: LP64
+      language: C
+  location:
+    file_name: dump1090.c
+    file_hash: de7cfc1fd2c72b08913bcac34637a8b24879904453d16ab46e2112fb034fb637
+    line: 4140
+    column: 5
+    function: main
+  location_invariant:
+    string: -1LL + (long long )j >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: dea896c1-2027-4697-ba4f-ceebd56ddf51
+    creation_time: 2024-08-11T07:43:15Z
+    producer:
+      name: Goblint
+      version: heads/michael-schwarz-dissertation-0-gccca4b23e-dirty
+      command_line: '''../../../analyzer/goblint'' ''--enable'' ''pre.keep'' ''--conf''
+        ''../../../analyzer/conf/traces-rel.json'' ''--set'' ''dbg.timeout'' ''1200''
+        ''--set'' ''ana.activated[+]'' ''threadJoins'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
+        ''witness.yaml.enabled'' ''dump1090.c'' ''--set'' ''witness.yaml.path'' ''dump1090_traces_rel.yml'''
+    task:
+      input_files:
+      - dump1090.c
+      input_file_hashes:
+        dump1090.c: de7cfc1fd2c72b08913bcac34637a8b24879904453d16ab46e2112fb034fb637
+      data_model: LP64
+      language: C
+  location:
+    file_name: dump1090.c
+    file_hash: de7cfc1fd2c72b08913bcac34637a8b24879904453d16ab46e2112fb034fb637
+    line: 4140
+    column: 5
+    function: main
+  location_invariant:
+    string: (0LL - (long long )argc) + (long long )j >= 0LL
+    type: assertion
+    format: C
diff --git a/concrat/fzy/main.c → concrat/fzy/fzy.c b/concrat/fzy/main.c → concrat/fzy/fzy.c
diff --git a/concrat/fzy/fzy_traces_rel.yml b/concrat/fzy/fzy_traces_rel.yml
@@ -0,0 +1 @@
+[]
diff --git a/concrat/klib/main.c → concrat/klib/klib.c b/concrat/klib/main.c → concrat/klib/klib.c
diff --git a/concrat/klib/klib_traces_rel.yml b/concrat/klib/klib_traces_rel.yml
@@ -0,0 +1,31 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: c54d70d8-0171-494c-98c3-11c37d6adc7c
+    creation_time: 2024-08-11T07:43:11Z
+    producer:
+      name: Goblint
+      version: heads/michael-schwarz-dissertation-0-gccca4b23e-dirty
+      command_line: '''../../../analyzer/goblint'' ''--enable'' ''pre.keep'' ''--conf''
+        ''../../../analyzer/conf/traces-rel.json'' ''--set'' ''dbg.timeout'' ''1200''
+        ''--set'' ''ana.activated[+]'' ''threadJoins'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''allglobs'' ''-v'' ''--enable''
+        ''witness.yaml.enabled'' ''klib.c'' ''--set'' ''witness.yaml.path'' ''klib_traces_rel.yml'''
+    task:
+      input_files:
+      - klib.c
+      input_file_hashes:
+        klib.c: 0dbc7a129339a8ba5ffa0555223e3b5055363deefe745ad33487cc5dd26ba76b
+      data_model: LP64
+      language: C
+  location:
+    file_name: klib.c
+    file_hash: 0dbc7a129339a8ba5ffa0555223e3b5055363deefe745ad33487cc5dd26ba76b
+    line: 521
+    column: 5
+    function: ktp_worker
+  location_invariant:
+    string: (long long )i >= 0LL
+    type: assertion
+    format: C
diff --git a/concrat/kona/main.c → concrat/kona/kona.c b/concrat/kona/main.c → concrat/kona/kona.c
diff --git a/concrat/level-ip/main.c → concrat/level-ip/level-ip.c b/concrat/level-ip/main.c → concrat/level-ip/level-ip.c