--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2016 ---
> [wp} user error: Builtin \cos(real) not defined > [wp] failure: Logic \cos undefined. We simply did not implement all built-ins in WP. One reason is that many SMT solvers (if not all) lack interesting properties about trigonometry. Workarounds: - either use another name, like âcosâ, and declare it using standard ACSL « logic real cos(real x); » within an axiomatic bloc, and add desired axioms and lemmas ; - or use a WP driver (WP manual § 2.4.10, p28) to bind `\cos` to some symbol in your favorite SMT solver (or Coq or Why3) ; for instance, see how we handle the â\maxâ function in '$(frama-c -print-share-path)/wp/wp.driverâ In all cases, consider using -wp-model float L.