diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-24 16:26:02 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-24 16:26:02 +0200 |
| commit | 011d9ef9a964a676380bb45195418595108e274b (patch) | |
| tree | ece2c02d2ec661e615284bf1d6e77fe4e5746225 /cfrontend/C2C.ml | |
| parent | 34768a3c2ed8a2ee09786cd7e56fe3a7e7491efb (diff) | |
| download | compcert-kvx-011d9ef9a964a676380bb45195418595108e274b.tar.gz compcert-kvx-011d9ef9a964a676380bb45195418595108e274b.zip | |
Remove ais_annot_intval.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 3e3ac48a..4c75c2f2 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -874,19 +874,6 @@ let rec convertExpr env e = ezero end - | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot_intval"}}, args) when Configuration.elf_target -> - begin match args with - | [ {edesc = C.EConst(CStr txt)}; arg ] -> - let targ = convertTyp env - (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(AST.EF_annot_val(P.of_int 2,coqstring_of_camlstring txt, typ_of_type targ), - Tcons(targ, Tnil), convertExprList env [arg], - convertTyp env e.etyp) - | _ -> - error "argument 1 of '__builtin_annot_intval' must be a string literal"; - ezero - end - | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) |