From 011d9ef9a964a676380bb45195418595108e274b Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 24 Oct 2017 16:26:02 +0200
Subject: Remove ais_annot_intval.

---
 cfrontend/C2C.ml | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'cfrontend')

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)
 
-- 
cgit