--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on July 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] making frama-c clang 0.0.5 fails with type error



Hi

I installed frama-clang the other day. You need this patch:

In file convert_acsl.ml, replace

let rec convert_logic_type env = function
  | Lvoid -> LTvoid
  | Lint ik -> LTint (convert_ikind ik)
  | Lfloat fk -> LTfloat (convert_fkind fk)
  | Larray (t,dim) ->
    let t = convert_logic_type env t in
    let dim = Extlib.opt_map convert_logic_constant dim in

by

let convert_cst_array_size env = function
  | LCInt v -> ASinteger v
  | LChr c | LWChr c -> ASinteger (string_of_int c)
  | LCEnum (_,s) ->
    let n, tk = Convert_env.typedef_normalize env s TStandard in
    let cname = Mangling.mangle n tk None in
    ASidentifier cname
  | LStr _ | LWStr _ | LCReal _ ->
    Frama_Clang_option.fatal "Unexpected value as array dimension"

let rec convert_logic_type env = function
  | Lvoid -> LTvoid
  | Lint ik -> LTint (convert_ikind ik)
  | Lfloat fk -> LTfloat (convert_fkind fk)
  | Larray (t,dim) ->
    let t = convert_logic_type env t in
    let dim =
      match dim with
      | Some dim -> convert_cst_array_size env dim
      | None -> ASnone
    in

Compilation should then terminate but you may then get this message when
you run frama-clang:

|:CommandLineError:Option'asm-macro-max-nesting-depth'registered more
than once! |

In which case, remove LLVMMCParser from USEDLIBS in file Makefile.clang.

Best regards

Nicky Williams


On 15/07/2018 16:02, Marius Melzer wrote:
> Hi,
>
> I wanted to try out the frama clang plugin following the instructions on
> [1]. I chose the most current version tar ball (0.0.5). On executing the
> "make" step, I get:
>
> File "convert_acsl.ml", line 90, characters 14-17:
> Error: This expression has type Logic_ptree.constant option
>        but an expression was expected of type Logic_ptree.array_size
> make: ***
> [/home/marius/.opam/4.05.0+flambda/share/frama-c/Makefile.generic:78:
> convert_acsl.cmo] Error 2
>
> What is the problem here?
>
> Thanks in advance,
> Marius
>
> [1] http://frama-c.com/frama-clang.html
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180716/76e8baa5/attachment.html>