Skip to content

Should assert always print source file & line number #1453

@Timmmm

Description

@Timmmm

Sail's assert() prints the file and line/column numbers but only if you don't add a message. I wonder if it should just always print them?

Currently the RISC-V model has this mess:

// This is all over the place:
internal_error(__FILE__, __LINE__, "should be unreachable");

val internal_error : forall ('a : Type). (string, int, string) -> 'a
function internal_error(file, line, s) = {
    assert (false, file ^ ":" ^ dec_str(line) ^ ": " ^ s);
    throw Error_internal_error()
}

It's pretty annoying to have to manually write __FILE__, __LINE__ (I think every time I've written this I copy/pasted it from somewhere else).

Also I don't know why it does a throw after assert(false). Can Sail asserts be disabled?

A built in unreachable("message") that is equivalent to assert(false, "message") would be neat too, given how many internal_error() calls we have.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions