From 82729353e53b05422a883b2a724e35fc87948379 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 14 Oct 2024 12:49:18 +0200
Subject: [PATCH 1/2] Add example where per function gas with maximum leads to
 non-termination

---
 .../80-context_gas/25-per-fun-nonterm.c       | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/regression/80-context_gas/25-per-fun-nonterm.c

diff --git a/tests/regression/80-context_gas/25-per-fun-nonterm.c b/tests/regression/80-context_gas/25-per-fun-nonterm.c
new file mode 100644
index 0000000000..4c3871688f
--- /dev/null
+++ b/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);
+}

From ce1866b6e61472957c13aac891b523712c2e46ae Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 14 Oct 2024 13:06:13 +0200
Subject: [PATCH 2/2] Fix per fundec gas

---
 src/lifters/contextGasLifter.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/lifters/contextGasLifter.ml b/src/lifters/contextGasLifter.ml
index 98974d81a1..75bd9f7641 100644
--- a/src/lifters/contextGasLifter.ml
+++ b/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