rems-project / cn-tutorial

7 stars 8 forks source link

Mod isn't supported #62

Closed lwli11 closed 1 month ago

lwli11 commented 1 month ago

The % operator is not supported, and the error message isn't explanatory:

The minimal program example capturing this is:

int mod(int n)
/*@
requires n>=0i32; n<MAXi32();
@*/
{
        return n % 2;
}

Which returns:

cn mod.c
[1/1]: mod
cn: internal error, uncaught exception:
    Failure("todo: Dune__exe__Check.check_pexpr")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 73, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 50, characters 8-11
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 50, characters 8-11
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 73, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 50, characters 8-11
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 73, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 50, characters 8-11
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 50, characters 8-11
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 50, characters 8-11
    Called from Dune__exe__Typing.run in file "backend/cn/typing.ml", line 66, characters 8-21
    Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 189, characters 20-87
    Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 185, characters 9-1023
    Re-raised at Dune__exe__Main.main in file "backend/cn/main.ml", line 231, characters 8-73
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
bcpierce00 commented 1 month ago

This one is very close to being fixed.

Message ID: @.***>

dc-mak commented 1 month ago

Thanks! Please report future CN-related issues on the above repo (for project tracking). I've created an issue there. (Also one can use backticks for pasting code dumps.)