[inferbo] Evaluation of abstract location of literal string

Summary:
It adds a semantics for evaluation of abstract location of literal
string, which was missing.

Reviewed By: mbouaziz

Differential Revision: D13915265

fbshipit-source-id: 741df843b

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -276,6 +276,8 @@ and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.t -> Va
 let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t =
  fun exp mem ->
   match exp with
+  | Const (Cstr s) ->
+      PowLoc.singleton (Loc.of_allocsite (Allocsite.literal_string s))
   | Var id ->
       Mem.find_stack (Var.of_id id |> Loc.of_var) mem |> Val.get_all_locs
   | Lvar pvar ->

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -198,6 +198,7 @@ codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bu
 codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset added: 8 Size: 4]
 codetoanalyze/c/bufferoverrun/models.c, strcpy_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 4 Size: 4]
 codetoanalyze/c/bufferoverrun/models.c, strcpy_contents_Bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/c/bufferoverrun/models.c, strcpy_literal_string_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 4 Size: 4]
 codetoanalyze/c/bufferoverrun/models.c, strcpy_no_null_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
 codetoanalyze/c/bufferoverrun/models.c, strcpy_strlen_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 4 Size: 4]
 codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -408,6 +408,16 @@ void strcpy_Bad() {
   strcpy(dst, src);
 }
 
+void strcpy_literal_string_Good() {
+  char dst[10];
+  strcpy(dst, "test");
+}
+
+void strcpy_literal_string_Bad() {
+  char dst[4];
+  strcpy(dst, "test");
+}
+
 void strcpy_strlen_Good() {
   char src[5] = "test";
   char dst[10];