Better doc/warnings and fix for last commit

README.md

@@ -231,8 +231,9 @@ using `\formal` should be surrounded by a
 When using the `\calling` context and targetting a specific called function, it
 is possible to refer to the value provided for a formal at every call site,
 using `\called_arg(parameter_name)`. It throws a type error when the called
-function does not have the specified formal, thus it should be surrounded by a
-[guard](#guarding-against-type-errors).
+function does not have the specified formal, is indirectly called (through a
+function pointer) or is a variadic function. Thus it should be surrounded by a
+[guard](#guarding-against-type-errors). 
 
 For example, the following meta-property states that parameter `x` of
 `float sqrt(float x)`

meta_annotate.ml

@@ -244,14 +244,22 @@ class calling_visitor flags all_mp table = object (self)
     let addr_term = addr_of_tlval called in
     let main_assoc = ("\\called", RepVariable addr_term) in
     let assoc_list = match called_kf with
-      | None -> [main_assoc]
+      | None ->
+        Self.warning ~once:true
+          "\\called_arg cannot be used with indirect calls" ;
+        [main_assoc]
       | Some kf ->
         let formals = Kernel_function.get_formals kf in
-        let param_assocs = List.map2 (fun formal given ->
-            let given_term = Logic_utils.expr_to_term given in
-            (formal.vorig_name, given_term)
-          ) formals args
-        in [main_assoc; ("\\called_arg", RepApp param_assocs)]
+        try
+          let param_assocs = List.map2 (fun formal given ->
+              let given_term = Logic_utils.expr_to_term given in
+              (formal.vorig_name, given_term)
+            ) formals args
+          in [main_assoc; ("\\called_arg", RepApp param_assocs)]
+        with Invalid_argument _ ->
+          Self.warning ~once:true "\\called_arg cannot be used with variadic \
+                                   functions. Please use the Instantiate plugin" ;
+          [main_assoc]
     in
     List.iter (self # instantiate stmt assoc_list) mp_todo
 

meta_parse.ml

@@ -88,7 +88,8 @@ let mp_contexts = [
 let mp_metavariables = [
   "\\written";
   "\\read";
-  "\\called"
+  "\\called";
+  "\\called_arg"
 ]
 let mp_utils = [
   "\\diff";
@@ -146,7 +147,8 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
       end
     | PLapp ("\\bound", _, [bound]) ->
       Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
-    | PLapp (app_name, _, [{lexpr_node = PLvar arg}]) ->
+    | PLapp (app_name, _, [{lexpr_node = PLvar arg}])
+      when List.mem app_name mp_terms ->
       begin match List.assoc_opt app_name termassoc with
         | Some RepApp l ->
           begin match List.assoc_opt arg l with

meta_parse.mli

@@ -54,8 +54,8 @@ type mp_translation =
   | MtNone
 
 type replaced_kind =
-  | RepVariable of term (* replace variable by term *)
-  | RepApp of (string * term) list (* replace application with arg by associated term *)
+  | RepVariable of term (** replace variable by term *)
+  | RepApp of (string * term) list (** replace application with arg by associated term *)
 
 type metaproperty = {
   mp_name : string;
@@ -69,5 +69,5 @@ type metaproperty = {
 
 val register_parsing : unit -> unit
 
-(* The list of meta-properties in the file, in the same order *)
+(** The list of meta-properties in the file, in the same order *)
 val metaproperties : unit -> metaproperty list

tests/meta-wp/oracle/uncalled.res.oracle

 [kernel] Parsing tests/meta-wp/uncalled.c (with preprocessing)
 [meta] Translation is enabled
 [meta] Will process 2 properties
+[meta] Warning: \called_arg cannot be used with indirect calls
 [meta] Successful translation
 [wp] Running WP plugin...
 [wp] tests/meta-wp/uncalled.c:21: Warning: Missing 'calls' for default behavior