Merge branch 'master' into svcomp-memsafety-benchmarks

goblint.opam

@@ -75,7 +75,6 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
   [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]

goblint.opam.locked

@@ -135,7 +135,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.2"
-    "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f"
+    "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331"
   ]
   [
     "ppx_deriving.5.2.1"

goblint.opam.template

@@ -2,7 +2,6 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
   [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]

src/analyses/base.ml

@@ -761,7 +761,8 @@ struct
         (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Z.to_string num) d_ikind ikind x | None -> ());
         Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
       | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
-      | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_const fkind num)
+      | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) && num = 0.0 -> Float (FD.of_const fkind num) (* constant 0 is ok, CIL creates these for zero-initializers; it is safe across float types *)
+      | Const (CReal (_, fkind, None)) when not (Cilfacade.isComplexFKind fkind) ->  assert false (* Cil does not create other CReal without string representation *)
       (* String literals *)
       | Const (CStr (x,_)) -> Address (AD.of_string x) (* normal 8-bit strings, type: char* *)
       | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)

src/analyses/libraryDesc.ml

@@ -58,6 +58,11 @@ type special =
   | Broadcast of Cil.exp
   | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
   | MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
+  (* All Sem specials  are not used yet. *)
+  | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; }
+  | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;}
+  | SemPost of Cil.exp
+  | SemDestroy of Cil.exp
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
   | Math of { fun_args: math; }

src/maingoblint.ml

@@ -412,14 +412,19 @@ let preprocess_files () =
   );
   preprocessed
 
+(** Regex for special "paths" in cpp output:
+    <built-in>, <command-line>, but also translations! *)
+let special_path_regexp = Str.regexp "<.+>"
+
 (** Parse preprocessed files *)
 let parse_preprocessed preprocessed =
   (* get the AST *)
   if get_bool "dbg.verbose" then print_endline "Parsing files.";
 
   let goblint_cwd = GobFpath.cwd () in
   let get_ast_and_record_deps (preprocessed_file, task_opt) =
-    let transform_file (path_str, system_header) = if Str.string_match (Str.regexp "<.+>") path_str 0 then
+    let transform_file (path_str, system_header) =
+      if Str.string_match special_path_regexp path_str 0 then
         (path_str, system_header) (* ignore special "paths" *)
       else
         let path = Fpath.v path_str in

src/util/cilfacade.ml

@@ -53,7 +53,8 @@ let init () =
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
   print_CIL_Input := true;
-  Cabs2cil.allowDuplication := false
+  Cabs2cil.allowDuplication := false;
+  Cabs2cil.silenceLongDoubleWarning := true
 
 let current_file = ref dummyFile
 

tests/regression/00-sanity/37-long-double.c

@@ -0,0 +1,4 @@
+int main() {
+  long double l = 0.0L;
+  return (int)l;
+}

tests/regression/00-sanity/37-long-double.t

@@ -0,0 +1,6 @@
+Testing that there isn't a warning about treating long double as double constant.
+  $ goblint 37-long-double.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3

tests/regression/28-race_reach/01-simple_racing.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -19,4 +20,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex2);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/02-simple_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -19,4 +20,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex1);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/03-munge_racing.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -26,4 +27,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/04-munge_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -26,4 +27,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/05-lockfuns_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -26,4 +27,4 @@ int main(void) {
   unlock();
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/06-cond_racing1.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include<stdio.h>
 #include<pthread.h>
 
@@ -31,7 +32,3 @@ int main() {
   join_threads(t);
   return 0;
 }
-
-
-
-

tests/regression/28-race_reach/07-cond_racing2.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include<stdio.h>
 #include<pthread.h>
 #include "racemacros.h"

tests/regression/28-race_reach/08-cond_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include<stdio.h>
 #include<pthread.h>
 #include "racemacros.h"

tests/regression/28-race_reach/09-ptrmunge_racing.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -27,4 +28,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/10-ptrmunge_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -27,4 +28,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/11-ptr_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -20,4 +21,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex2);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/12-ptr_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -16,8 +17,8 @@ void *t_fun(void *arg) {
 int main(void) {
   create_threads(t);
   pthread_mutex_lock(&mutex1);
-  assert_racefree(global); 
+  assert_racefree(global);
   pthread_mutex_unlock(&mutex1);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/19-callback_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>

tests/regression/28-race_reach/20-callback_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>

tests/regression/28-race_reach/21-deref_read_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/22-deref_read_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/23-sound_unlock_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/24-sound_lock_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/27-funptr_racing.c

@@ -1,15 +1,16 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include <stdio.h>
 #include "racemacros.h"
 
 int global;
 pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER;
 
-void bad() { 
+void bad() {
   access(global);
 }
 
-void good() { 
+void good() {
   pthread_mutex_lock(&gm);
   access(global);
   pthread_mutex_unlock(&gm);
@@ -42,4 +43,4 @@ int main() {
 
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/28-funptr_racefree.c

@@ -1,14 +1,15 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include <stdio.h>
 #include "racemacros.h"
 
 int global = 0;
 pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER;
 
-void bad() { 
+void bad() {
   access(global);
-} 
-void good() { 
+}
+void good() {
   pthread_mutex_lock(&gm);
   access(global);
   pthread_mutex_unlock(&gm);
@@ -41,4 +42,4 @@ int main() {
 
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/36-indirect_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/37-indirect_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/40-trylock_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -25,4 +26,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex); // no UB because ERRORCHECK
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/41-trylock_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -22,4 +23,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/42-trylock2_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -35,4 +36,4 @@ int main(void) {
 
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/45-escape_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/46-escape_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/51-mutexptr_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/60-invariant_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/61-invariant_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/70-funloop_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/71-funloop_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/72-funloop_hard_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"