From 300a195840ef9d4db014aaef9de6f3c1224fb563 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 20 Sep 2024 18:13:18 +0200 Subject: [PATCH] Complete `thread_gas` --- src/framework/constraints.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 5bc83fbe13..ce10393d06 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -542,7 +542,12 @@ module PerFunctionGas(GasVal:GasVal):Gas = struct let callee_gas f v = let c = Option.default (G.top ()) (M.find_opt f v) in M.add f (max 0 c-1) v - let thread_gas f v = v (* max 0 (v - 1) *) + let thread_gas f v = + match Cilfacade.find_varinfo_fundec f with + | fd -> + callee_gas fd v + | exception Not_found -> + callee_gas Cil.dummyFunDec v end