diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index d7e9b2bffb148b1f717cb3e466a39cd54316320a..08661199e82138508e48acce0a21c7ece08ebe89 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -38,6 +38,12 @@ let infer_intervals = true
    minimal drop in efficiency. *)
 let saturate_octagons = true
 
+(* Is the domain intraprocedural, according to the -eva-octagons-through-calls
+   option. In this case, the analysis of each function starts with an empty
+   state, and the relations inferred in a function are not propagated back to
+   the caller either. *)
+let intraprocedural () = not (Value_parameters.OctagonsCall.get ())
+
 (* -------------------------------------------------------------------------- *)
 (*                  Basic types: pair of variables and Ival.t                 *)
 (* -------------------------------------------------------------------------- *)
@@ -1190,11 +1196,22 @@ module Domain = struct
 
     let assume _stmt _exp _bool = update
 
-    let start_call _stmt _call _valuation _state = `Value (empty ())
+    let start_call _stmt call valuation state =
+      if intraprocedural ()
+      then `Value (empty ())
+      else
+        let state = { state with modified = Locations.Zone.bottom } in
+        let assign_formal state { formal; concrete; avalue } =
+          state >>- assign_variable formal concrete avalue valuation
+        in
+        List.fold_left assign_formal (`Value state) call.arguments
 
     let finalize_call _stmt _call ~pre ~post =
-      let written_zone = post.modified in
-      `Value (kill written_zone pre)
+      if intraprocedural ()
+      then `Value (kill post.modified pre)
+      else
+        let modified = Locations.Zone.join post.modified pre.modified in
+        `Value { post with modified }
 
     let show_expr _valuation _state _fmt _expr = ()
   end
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index dd13a4af2beef0df0fc9bf9b1153afd22bbfc19c..f283790bf96b2f97752e9cca4a1cf2361c78625c 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -319,6 +319,21 @@ module EqualityCallFunction =
     end)
 let () = add_precision_dep EqualityCallFunction.parameter
 
+let () = Parameter_customize.set_group domains
+module OctagonsCall =
+  Bool
+    (struct
+      let option_name = "-eva-octagons-through-calls"
+      let help = "Whether the relations inferred by the octagons domain are \
+                  propagated through function calls. Disabled by default: \
+                  the octagons analysis is intra-procedural, starting \
+                  each function with an empty octagons state, \
+                  and losing the octagons inferred at the end. \
+                  The interprocedural analysis is more precise but slower."
+      let default = false
+    end)
+let () = add_precision_dep OctagonsCall.parameter
+
 let () = Parameter_customize.set_group domains
 module Numerors_Real_Size =
   Int
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index edc7a34b9042010629f594db8e81f468393df135..84ec6ea9a83c41ed82e83c22cafceeb88853e7de 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -51,6 +51,8 @@ module EqualityCallFunction:
   Parameter_sig.Map with type key = Cil_types.kernel_function
                      and type value = string
 
+module OctagonsCall: Parameter_sig.Bool
+
 module TracesUnrollLoop: Parameter_sig.Bool
 module TracesUnifyLoop: Parameter_sig.Bool
 module TracesDot: Parameter_sig.String