Skip to content

Paper cuts

This issue collects known problems in RefinedC that can be worked around but should be fixed at some point.

  • guarded is only striped on struct field access, not on pointer dereference. This leads to weird error messages and more annotations, see e.g. here
    Workaround: use rc_unfold

Done:

  • !p where p is a pointer is currently not supported by the frontend (workaround: use p == NULL). Fixed by !100 (merged).
  • find_in_context_type_val_P_own_singleton can lead to infinite loops in failing cases Fixed in cd997eef via place' type
  • && and || are only supported inside if statements with desugaring in the frontend, but they should be provided by notation.v (via IfE). Fixed by !97 (merged).
  • Support for the comma operator. Fixed by 2c7772a9.
  • p++ where p is a pointer generates an assertion failure in the frontend (e.g. int i; int *ip = &i; ip++;). Workaround: use p += 1. Fixed by 98393de0.
  • The ternary operator is not supported (adding a ternary operator expression that does not include function calls should be doable)
    Workaround: rewrite the code to use if, fixed by 2933e60f
  • ensure that the automation destructs all tuples (including those coming from parameters). Ideally figure out how to give good names, but that is probably not possible in general. Fixed by 95ee66c9.
  • "Operand types not uniform for comparing operator." This error occurs if the arguments of a comparison operator don't have the same (integer?) type, e.g. (int) x == (size_t) x. It also occurs implicitly through the use of !x which is desugared to x == 0 by the frontend. Fixed by 7783f187
  • All structs require a rc::refined_by annotation. Sometimes it would be nice if an omitted rc::refined_by annotation would be inferred as rc::refined_by("_ : unit").
    Workaround: add the refined_by annotation Fixed by 2d10ddb7
  • Global variables with names that are Coq identifiers (like end) lead to strange errors
    Workaround: rename the global variable Fixed by !11 (merged)
  • Annotations using global_at_type are quite ugly currently. @lepigre suggested supporting something like [[rc::requires("global cur1 : &own<uninit<{ly_set_size PAGE_LAYOUT n}>>")]] in the frontend instead of [[rc::requires("[global_with_type \"cur1\" Own (&own (uninit (ly_set_size PAGE_LAYOUT n)))]")]].
Edited by Michael Sammler