Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>