Merge pull request #1598 from goblint/gas_fundec_needs_to_be_min

⛽: Use minimum to combine incoming gas values in per-context gas

src/lifters/contextGasLifter.ml

@@ -121,12 +121,15 @@ let get_gas_lifter () =
     (module ContextGasLifter(GlobalGas):Spec2Spec)
   else
     let module PerFunctionGas:Gas = struct
-      module G = GasChain
-      module M = MapDomain.MapTop_LiftBot(CilType.Fundec)(G)
+      (* The order is reversed here to ensure that the minimum is used *)
+      (* 5 join 4 = 4 *)
+      module G = Lattice.Reverse(GasChain)
+      (* Missing bindings are bot, i.e., have maximal gas for this function *)
+      module M = MapDomain.MapBot_LiftTop(CilType.Fundec)(G)
       let startgas () = M.empty ()
       let is_exhausted f v = GobOption.exists (fun g -> g <= 0) (M.find_opt f v)  (* v <= 0 *)
       let callee_gas f v =
-        let c = Option.default (G.top ()) (M.find_opt f v) in
+        let c = Option.default (G.bot ()) (M.find_opt f v) in
         M.add f (max 0 c-1) v
       let thread_gas f v =
         match Cilfacade.find_varinfo_fundec f with

tests/regression/80-context_gas/25-per-fun-nonterm.c

@@ -0,0 +1,29 @@
+//PARAM: --enable ana.int.interval_set --set ana.context.gas_value 3 --set ana.context.gas_scope function
+// NOTIMEOUT
+void h(int n) {
+    int x;
+
+    if(x) {
+        return;
+    }
+
+    g(n+1);
+    h(n+1);
+}
+
+void g(int n) {
+    int x;
+
+    if(x) {
+        return;
+    }
+
+    g(n+1);
+    h(n+1);
+}
+
+int main()
+{
+    g(0);
+    h(0);
+}