Add expression location to return

src/check.ml

@@ -760,8 +760,9 @@ and checkStmt (s: stmt) =
           currentLoc := l;
           let te = checkExp false e in
           typeMatch te voidPtrType
-      | Return (re,l) -> begin
+      | Return (re, l, el) -> begin
           currentLoc := l;
+          currentExpLoc := el;
           match re, !currentReturnType with
             None, TVoid _  -> ()
           | _, TVoid _ -> ignore (warn "Invalid return value")

src/cil.ml

@@ -767,8 +767,9 @@ and stmtkind =
   | Instr  of instr list               (** A group of instructions that do not
                                            contain control flow. Control
                                            implicitly falls through. *)
-  | Return of exp option * location     (** The return statement. This is a
-                                            leaf in the CFG. *)
+  | Return of exp option * location * location (** The return statement. This is a
+                                                   leaf in the CFG.
+                                                   Second location is just for expression. *)
 
   | Goto of stmt ref * location         (** A goto statement. Appears from
                                             actual goto's in the code. *)
@@ -1145,7 +1146,7 @@ let rec get_stmtLoc (statement : stmtkind) =
   match statement with
       Instr([]) -> lu
     | Instr(hd::tl) -> get_instrLoc(hd)
-    | Return(_, loc) -> loc
+    | Return(_, loc, _) -> loc
     | Goto(_, loc) -> loc
     | ComputedGoto(_, loc) -> loc
     | Break(loc) -> loc
@@ -3861,11 +3862,11 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           ++ self#pBlock () thenBlock)
 
   method private pStmtKind (next: stmt) () = function
-      Return(None, l) ->
+      Return(None, l, el) ->
         self#pLineDirective l
           ++ text "return;"
 
-    | Return(Some e, l) ->
+    | Return(Some e, l, el) ->
         self#pLineDirective l
           ++ text "return ("
           ++ self#pExp () e
@@ -5363,13 +5364,13 @@ and childrenStmt (toPrepend: instr list ref) : cilVisitor -> stmt -> stmt =
   (* Just change the statement kind *)
   let skind' =
     match s.skind with
-      Break _ | Continue _ | Goto _ | Return (None, _) -> s.skind
+      Break _ | Continue _ | Goto _ | Return (None, _, _) -> s.skind
     | ComputedGoto (e, l) ->
          let e' = fExp e in
          if e' != e then ComputedGoto (e', l) else s.skind
-    | Return (Some e, l) ->
+    | Return (Some e, l, el) ->
         let e' = fExp e in
-        if e' != e then Return (Some e', l) else s.skind
+        if e' != e then Return (Some e', l, el) else s.skind
     | Loop (b, l, el, s1, s2) ->
         let b' = fBlock b in
         if b' != b then Loop (b', l, el, s1, s2) else s.skind

src/cil.mli

@@ -964,8 +964,9 @@ and stmtkind =
   (** A group of instructions that do not contain control flow. Control
      implicitly falls through. *)
 
-  | Return of exp option * location
-   (** The return statement. This is a leaf in the CFG. *)
+  | Return of exp option * location * location
+   (** The return statement. This is a leaf in the CFG.
+       Second location is just for expression. *)
 
   | Goto of stmt ref * location
    (** A goto statement. Appears from actual goto's in the code or from

src/ext/dataslicing/dataslicing.ml

@@ -336,16 +336,16 @@ let sliceInstr (inst : instr) : instr list =
       instrs @ (Call (ret', sliceExp 1 fn, args', l, el) :: set)
   | _ -> E.s (unimp "inst %a" d_instr inst)
 
-let sliceReturnExp (eo : exp option) (l : location) : stmtkind =
+let sliceReturnExp (eo : exp option) (l : location) (el : location) : stmtkind =
   match eo with
   | Some e ->
       begin
       match sliceExpAll e l with
-      | [], e' -> Return (Some e', l)
+      | [], e' -> Return (Some e', l, el)
       | instrs, e' -> Block (mkBlock [mkStmt (Instr instrs);
-                                      mkStmt (Return (Some e', l))])
+                                      mkStmt (Return (Some e', l, el))])
       end
-  | None -> Return (None, l)
+  | None -> Return (None, l, el)
 
 let rec sliceStmtKind (sk : stmtkind) : stmtkind =
   match sk with
@@ -354,7 +354,7 @@ let rec sliceStmtKind (sk : stmtkind) : stmtkind =
   | If (e, b1, b2, l, el) -> If (sliceExp 1 e, sliceBlock b1, sliceBlock b2, l, el)
   | Break l -> Break l
   | Continue l -> Continue l
-  | Return (eo, l) -> sliceReturnExp eo l
+  | Return (eo, l, el) -> sliceReturnExp eo l el
   | Switch (e, b, sl, l, el) -> Switch (sliceExp 1 e, sliceBlock b,
                                     Util.list_map sliceStmt sl, l, el)
   | Loop (b, l, el, so1, so2) -> Loop (sliceBlock b, l, el,

src/ext/liveness/usedef.ml

@@ -190,8 +190,8 @@ let computeUseDefStmtKind ?(acc_used=VS.empty)
   let ve e = ignore (visitCilExpr useDefVisitor e) in
   let _ =
     match sk with
-      Return (None, _) -> ()
-    | Return (Some e, _) -> ve e
+      Return (None, _, _) -> ()
+    | Return (Some e, _, _) -> ve e
     | If (e, _, _, _, _) -> ve e
     | Break _ | Goto _ | Continue _ -> ()
     | ComputedGoto (e, _) -> ve e
@@ -218,8 +218,8 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty)
   varDefs := acc_defs;
   let ve e = ignore (visitCilExpr useDefVisitor e) in
   match sk with
-    Return (None, _) -> !varUsed, !varDefs
-  | Return (Some e, _) ->
+    Return (None, _, _) -> !varUsed, !varDefs
+  | Return (Some e, _, _) ->
       let _ = ve e in
       !varUsed, !varDefs
   | If (e, tb, fb, _, _) ->

src/ext/pta/ptranal.ml

@@ -304,7 +304,7 @@ let analyze_instr (i : instr ) : unit =
 let rec analyze_stmt (s : stmt ) : unit =
   match s.skind with
       Instr il -> List.iter analyze_instr il
-    | Return (eo, l) ->
+    | Return (eo, l, el) ->
         begin
           match eo with
               Some e ->

src/ext/syntacticsearch/funcFunction.ml

@@ -32,7 +32,7 @@ class fun_find_returns funname funid result : nopCilVisitor =
 
     method! vstmt stmt =
       match stmt.skind with
-      | Return (Some exp, loc) ->
+      | Return (Some exp, loc, eloc) ->
           result :=
             !result
             @ [
@@ -42,7 +42,7 @@ class fun_find_returns funname funid result : nopCilVisitor =
                   -1 );
               ];
           DoChildren
-      | Return (None, loc) ->
+      | Return (None, loc, eloc) ->
           result := !result @ [ ("", loc, "void", -1) ];
           DoChildren
       | _ -> DoChildren
@@ -72,7 +72,7 @@ class fun_find_sig funname funid result : nopCilVisitor =
 
     method! vstmt stmt =
       match stmt.skind with
-      | Return (Some exp, loc) ->
+      | Return (Some exp, loc, eloc) ->
           result :=
             !result
             @ [
@@ -82,7 +82,7 @@ class fun_find_sig funname funid result : nopCilVisitor =
                   -1 );
               ];
           SkipChildren
-      | Return (None, loc) ->
+      | Return (None, loc, eloc) ->
           result := !result @ [ ("", loc, "void", -1) ];
           SkipChildren
       | _ -> DoChildren

src/ext/syntacticsearch/funcVar.ml

@@ -170,7 +170,7 @@ let rec search_stmt_list_for_var list name varid includeCallTmp =
       ( match x.skind with
       | Instr ins_list ->
           search_instr_list_for_var ins_list name varid includeCallTmp
-      | Return (Some exp, loc) ->
+      | Return (Some exp, loc, eloc) ->
           search_expression exp name loc varid includeCallTmp
       | ComputedGoto (exp, loc) ->
           search_expression exp name loc varid includeCallTmp

src/formatparse.mly

@@ -1334,7 +1334,7 @@ stmt:
                   }
 |   RETURN exp_opt SEMICOLON
                   { (fun mkTemp loc args ->
-                         mkStmt (Return((fst $2) args, loc)))
+                         mkStmt (Return((fst $2) args, loc, locUnknown))) (* TODO: better eloc *)
                   }
 |   BREAK SEMICOLON
                   { (fun mkTemp loc args ->

src/frontc/cabs.ml

@@ -223,7 +223,7 @@ and statement =
  | FOR of for_clause * expression * expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | BREAK of cabsloc
  | CONTINUE of cabsloc
- | RETURN of expression * cabsloc
+ | RETURN of expression * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | SWITCH of expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | CASE of expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | CASERANGE of expression * expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)

src/frontc/cabs2cil.ml

@@ -859,7 +859,7 @@ module BlockChunk =
           let doLoc = if first then fun x -> x else doLoc in
           s.skind <- match s.skind with
             | Instr xs -> Instr (doInstrs ~first xs)
-            | Return (e, loc) -> Return (e, doLoc loc)
+            | Return (e, loc, eloc) -> Return (e, doLoc loc, doLoc eloc)
             | Goto (s, loc) -> Goto (s, doLoc loc)
             | ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc)
             | Break loc -> Break (doLoc loc)
@@ -907,7 +907,7 @@ module BlockChunk =
         let rec doStmt s: unit =
           s.skind <- match s.skind with
             | Instr xs -> Instr (doInstrs xs)
-            | Return (e, loc) -> Return (e, doLoc loc)
+            | Return (e, loc, eloc) -> Return (e, doLoc loc, doLoc eloc)
             | Goto (s, loc) -> Goto (s, doLoc loc)
             | ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc)
             | Break loc -> Break (doLoc loc)
@@ -973,8 +973,8 @@ module BlockChunk =
 
     let skipChunk = empty
 
-    let returnChunk (e: exp option) (l: location) : chunk =
-      { stmts = [ mkStmt (Return(e, l)) ];
+    let returnChunk (e: exp option) (l: location) (el: location) : chunk =
+      { stmts = [ mkStmt (Return(e, l, el)) ];
         postins = [];
         cases = []
       }
@@ -5919,7 +5919,7 @@ and doAliasFun vtype (thisname:string) (othername:string)
                (argsToList formals) in
   let call = A.CALL (A.VARIABLE othername, args) in
   let stmt = if isVoidType rt then A.COMPUTATION(call, loc)
-                              else A.RETURN(call, loc)
+                              else A.RETURN(call, loc, loc)
   in
   let body = { A.blabels = []; A.battrs = []; A.bstmts = [stmt] } in
   let fdef = A.FUNDEF (sname, body, loc, loc) in
@@ -6471,7 +6471,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
               then
                 !currentFunctionFDEC.sbody.bstmts <-
                   !currentFunctionFDEC.sbody.bstmts
-                  @ [mkStmt (Return(retval, endloc))]
+                  @ [mkStmt (Return(retval, endloc, locUnknown))]
             end;
 
             (* ignore (E.log "The env after finishing the body of %s:\n%t\n"
@@ -6769,29 +6769,32 @@ and doStatement (s : A.statement) : chunk =
         currentLoc := loc';
         continueOrLabelChunk loc'
 
-    | A.RETURN (A.NOTHING, loc) ->
+    | A.RETURN (A.NOTHING, loc, eloc) ->
         let loc' = convLoc loc in
+        let eloc' = convLoc eloc in
         currentLoc := loc';
+        currentExpLoc := eloc';
         if not (isVoidType !currentReturnType) then
           ignore (warn "Return statement without a value in function returning %a" d_type !currentReturnType);
-        returnChunk None loc'
+        returnChunk None loc' eloc'
 
-    | A.RETURN (e, loc) ->
+    | A.RETURN (e, loc, eloc) ->
         let loc' = convLoc loc in
+        let eloc' = convLoc eloc in
         currentLoc := loc';
-        currentExpLoc := loc'; (* TODO: separate expression loc *)
+        currentExpLoc := eloc';
         (* Sometimes we return the result of a void function call *)
         if isVoidType !currentReturnType then begin
           ignore (warnOpt "Return statement with a value in function returning void");
           let (se, _, _) = doExp false e ADrop in
-          se @@ returnChunk None loc'
+          se @@ returnChunk None loc' eloc'
         end else begin
 	  let rt =
 	    typeRemoveAttributes ["warn_unused_result"] !currentReturnType
 	  in
           let (se, e', et) = doExp false e (AExp (Some rt)) in
           let (et'', e'') = castTo et rt e' in
-          se @@ (returnChunk (Some e'') loc')
+          se @@ (returnChunk (Some e'') loc' eloc')
         end
 
     | A.SWITCH (e, s, loc, eloc) ->

src/frontc/cabshelper.ml

@@ -93,7 +93,7 @@ begin
   | FOR(_,_,_,_,loc,_) -> loc
   | BREAK(loc) -> loc
   | CONTINUE(loc) -> loc
-  | RETURN(_,loc) -> loc
+  | RETURN(_,loc,_) -> loc
   | SWITCH(_,_,loc,_) -> loc
   | CASE(_,_,loc,_) -> loc
   | CASERANGE(_,_,_,loc,_) -> loc

src/frontc/cabsvisit.ml

@@ -393,9 +393,9 @@ and childrenStatement vis s =
       if fc1' != fc1 || e2' != e2 || e3' != e3 || s4' != s4
       then FOR (fc1', e2', e3', s4', l, el) else s
   | BREAK _ | CONTINUE _ | GOTO _ -> s
-  | RETURN (e, l) ->
+  | RETURN (e, l, el) ->
       let e' = ve e in
-      if e' != e then RETURN (e', l) else s
+      if e' != e then RETURN (e', l, el) else s
   | SWITCH (e, s1, l, el) ->
       let e' = ve e in
       let s1' = vs l s1 in

src/frontc/cparser.mly

@@ -972,9 +972,9 @@ statement_no_null:
 	                         {CASERANGE (fst $2, fst $4, $6, joinLoc $1 $7, joinLoc $1 $5)}
 |   DEFAULT COLON statement location
 	                         {DEFAULT ($3, joinLoc $1 $4, joinLoc $1 $2)}
-|   RETURN SEMICOLON		 {RETURN (NOTHING, joinLoc $1 $2)}
+|   RETURN SEMICOLON		 {RETURN (NOTHING, joinLoc $1 $2, cabslu)}
 |   RETURN comma_expression SEMICOLON
-	                         {RETURN (smooth_expression (fst $2), joinLoc $1 $3)}
+	                         {RETURN (smooth_expression (fst $2), joinLoc $1 $3, joinLoc (snd $2) $3)}
 |   BREAK SEMICOLON     {BREAK (joinLoc $1 $2)}
 |   CONTINUE SEMICOLON	 {CONTINUE (joinLoc $1 $2)}
 |   GOTO IDENT SEMICOLON

src/frontc/cprint.ml

@@ -650,7 +650,7 @@ and print_statement stat =
   | CONTINUE (loc) ->
       setLoc(loc);
       print "continue;"; new_line ()
-  | RETURN (exp, loc) ->
+  | RETURN (exp, loc, eloc) ->
       setLoc(loc);
       print "return";
       if exp = NOTHING