diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-07-04 14:01:06 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-07-04 14:01:06 +0200 |
| commit | 8dc7fb147fb49294ccc4357b0c566b7e007c680f (patch) | |
| tree | feccdae56d938588c5c122611a47eae4aa62f92e | |
| parent | debbae89f9faf47b95bd1c86058cd232783f3c3f (diff) | |
| download | compcert-8dc7fb147fb49294ccc4357b0c566b7e007c680f.tar.gz compcert-8dc7fb147fb49294ccc4357b0c566b7e007c680f.zip | |
Deref is not safe.
| -rw-r--r-- | cparser/Checks.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/Checks.ml b/cparser/Checks.ml index e79e3ccf..a2602a52 100644 --- a/cparser/Checks.ml +++ b/cparser/Checks.ml @@ -317,7 +317,7 @@ let safe_expr vars env e = | Oderef -> begin match e.edesc with | EUnop (Oaddrof,e) -> expr e - | _ -> expr e + | _ -> false end (* e.f is okay if f has array or composite type *) | Odot m -> |