diff --git a/ivette/src/dome/renderer/frame/sidebars.tsx b/ivette/src/dome/renderer/frame/sidebars.tsx index e8ceaeb196bef6d7e9241c19ff4b5d8ec9a024c2..c91e9dfa812fd06be6b7406ce9c916e4f6593a10 100644 --- a/ivette/src/dome/renderer/frame/sidebars.tsx +++ b/ivette/src/dome/renderer/frame/sidebars.tsx @@ -32,7 +32,7 @@ import React from 'react'; import { useFlipSettings } from 'dome'; import { Badge } from 'dome/controls/icons'; -import { Label } from 'dome/controls/labels'; +import { Label, Title } from 'dome/controls/labels'; import { classes } from 'dome/misc/utils'; import { Hbox } from 'dome/layout/boxes'; import { IconButton, IconButtonProps } from 'dome/controls/buttons'; @@ -261,3 +261,30 @@ export function Item(props: ItemProps): JSX.Element { } // -------------------------------------------------------------------------- +// --- SideBar Title +// -------------------------------------------------------------------------- + +export interface SidebarTitleProps { + /** Label. */ + label: string; + /** Additionnal CSS class. */ + className?: string; + /** Other elements. */ + children?: React.ReactNode; +} + +/** Sidebar Title. */ +export function SidebarTitle(props: SidebarTitleProps): JSX.Element { + const { label, children } = props; + const className = classes( + 'dome-xSideBarTitle', + props.className, + ); + return ( + <Hbox className={className}> + <Hbox><Title label={label} title={label}/></Hbox> + { children} + </Hbox> + ); +} +// -------------------------------------------------------------------------- diff --git a/ivette/src/dome/renderer/frame/style.css b/ivette/src/dome/renderer/frame/style.css index 01924730df603a035e3a3b46e7b9e14a3c225f08..3e76ba41171f6cb3013f47324cdf617abe8ee38e 100644 --- a/ivette/src/dome/renderer/frame/style.css +++ b/ivette/src/dome/renderer/frame/style.css @@ -90,22 +90,28 @@ overflow-x: hidden ; overflow-y: auto ; padding: 0px ; -} -.dome-xSideBar.dome-color-frame -{ - background: var(--background-sidebar) ; + &.dome-color-frame { + background: var(--background-sidebar); + } - .dome-xSideBar-title { + .dome-xSideBarTitle { + flex-wrap: wrap; justify-content: space-between; position:sticky; top:0; z-index: 10; padding: 5px; border-bottom: solid 1px var(--border-discrete); - background-color:var(--background-sidebar); + + .dome-xBoxes-hbox { + max-width: 100%; + flex-wrap: wrap; + align-content: center; + } } } + /* -------------------------------------------------------------------------- */ /* --- SideBar Section --- */ /* -------------------------------------------------------------------------- */ diff --git a/ivette/src/frama-c/kernel/Globals.tsx b/ivette/src/frama-c/kernel/Globals.tsx index a029711994588429a81f1e6a6608c8ce49c315bd..0bb22020345a6f400666c0685efb99d88c866a64 100644 --- a/ivette/src/frama-c/kernel/Globals.tsx +++ b/ivette/src/frama-c/kernel/Globals.tsx @@ -29,9 +29,9 @@ import * as Dome from 'dome'; import * as Json from 'dome/data/json'; import { classes } from 'dome/misc/utils'; import { alpha } from 'dome/data/compare'; -import { Section, Item } from 'dome/frame/sidebars'; +import { Section, Item, SidebarTitle } from 'dome/frame/sidebars'; import { Button } from 'dome/controls/buttons'; -import { Label, Title } from 'dome/controls/labels'; +import { Label } from 'dome/controls/labels'; import * as Toolbar from 'dome/frame/toolbars'; import { Hbox } from 'dome/layout/boxes'; import InfiniteScroll from 'react-infinite-scroller'; @@ -686,37 +686,36 @@ function SidebarFilesTitle(props: SidebarFilesTitleProps): JSX.Element { const [showFcts, flipShowFcts] = showFctsState; const [showVars, flipShowVars] = showVarsState; - return <Hbox className='dome-xSideBar-title' > - <Hbox style={{ flexWrap: 'wrap', alignContent: 'center' }}> - <Title label='Files' /> - </Hbox> - <Hbox> - <Toolbar.ButtonGroup> - <Toolbar.Button - icon="FUNCTION" - title={'Show functions'} - selected={showFcts} - onClick={() => flipShowFcts()} - /> - <Toolbar.Button - icon='TUNINGS' - onClick={() => Dome.popupMenu(contextFctMenuItems)} - /> - </Toolbar.ButtonGroup> - <Toolbar.ButtonGroup> - <Toolbar.Button - icon="VARIABLE" - title={'Show variables'} - selected={showVars} - onClick={() => flipShowVars()} - /> - <Toolbar.Button - icon='TUNINGS' - onClick={() => Dome.popupMenu(contextVarMenuItems)} - /> - </Toolbar.ButtonGroup> - </Hbox> - </Hbox>; + return ( + <SidebarTitle label='Files'> + <Hbox> + <Toolbar.ButtonGroup> + <Toolbar.Button + icon="FUNCTION" + title={'Show functions'} + selected={showFcts} + onClick={() => flipShowFcts()} + /> + <Toolbar.Button + icon='TUNINGS' + onClick={() => Dome.popupMenu(contextFctMenuItems)} + /> + </Toolbar.ButtonGroup> + <Toolbar.ButtonGroup> + <Toolbar.Button + icon="VARIABLE" + title={'Show variables'} + selected={showVars} + onClick={() => flipShowVars()} + /> + <Toolbar.Button + icon='TUNINGS' + onClick={() => Dome.popupMenu(contextVarMenuItems)} + /> + </Toolbar.ButtonGroup> + </Hbox> + </SidebarTitle> + ); } // -------------------------------------------------------------------------- @@ -757,12 +756,14 @@ export function GlobalByFiles(): JSX.Element { export function GlobalDeclarations(): JSX.Element { const scrollableArea = React.useRef<HTMLDivElement>(null); - return ( - <div ref={scrollableArea} className="globals-scrollable-area"> - <Types /> - <Variables scrollableParent={scrollableArea} /> - <Functions scrollableParent={scrollableArea} /> - </div> + return (<> + <SidebarTitle label='Global Declarations' /> + <div ref={scrollableArea} className="globals-scrollable-area"> + <Types /> + <Variables scrollableParent={scrollableArea} /> + <Functions scrollableParent={scrollableArea} /> + </div> + </> ); } diff --git a/ivette/src/frama-c/plugins/eva/components/Tools.tsx b/ivette/src/frama-c/plugins/eva/components/Tools.tsx index c13fe32c852a0c74ade024b8223f1c2196a6bd2f..d876454889f6ac283a644236a201facdbc873df9 100644 --- a/ivette/src/frama-c/plugins/eva/components/Tools.tsx +++ b/ivette/src/frama-c/plugins/eva/components/Tools.tsx @@ -28,6 +28,7 @@ import * as Server from 'frama-c/server'; import * as States from 'frama-c/states'; import * as Eva from 'frama-c/plugins/eva/api/general'; import { EvaStatus } from 'frama-c/plugins/eva/components/AnalysisStatus'; +import { SidebarTitle } from 'dome/frame/sidebars'; export interface EvaToolsProps { @@ -60,7 +61,7 @@ export default function EvaTools( const syncToFC = (): void => { remote.commit(); }; return ( - <Hbox className='dome-xSideBar-title eva-tools'> + <SidebarTitle label='Parameters of Eva Analysis' className='eva-tools'> <Hbox className='eva-tools-actions'> <IconButton icon="MEDIA.PLAY" @@ -100,6 +101,6 @@ export default function EvaTools( <Hbox className='eva-tools-status'> <EvaStatus iconSize={18} /> </Hbox> - </Hbox> + </SidebarTitle> ); } diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css index 2821d3ff355a85cdf99291880aca3a17b77a4432..3823792c67e26651a907f917638c0285d65fe9ce 100644 --- a/ivette/src/frama-c/plugins/eva/style.css +++ b/ivette/src/frama-c/plugins/eva/style.css @@ -358,12 +358,6 @@ tr:first-of-type > .eva-table-callsite-box { /* ------------------ */ /* --- Tools Eva --- */ .eva-tools { - - .eva-tools-actions { - display: flex; - flex-wrap: wrap; - } - .dome-xIconButton { padding: 2px 5px; } diff --git a/ivette/src/ivette/laboratory.tsx b/ivette/src/ivette/laboratory.tsx index 29026cd02670dccb8a5c7255854b27d6cefa2483..2471017c620d3fdd00ee1c23450c94e2ee663375 100644 --- a/ivette/src/ivette/laboratory.tsx +++ b/ivette/src/ivette/laboratory.tsx @@ -1223,8 +1223,8 @@ function ViewBar(): JSX.Element { const groups = State.useElements(GROUP); const allGroups = groups.concat(Sandbox); - return ( - <Sidebars.SideBar> + return (<> + <Sidebars.SidebarTitle label='Views & Components' /> <ViewSection key='views' /> {groups.map((group) => <GroupSection @@ -1236,7 +1236,7 @@ function ViewBar(): JSX.Element { <GroupSection key='sandbox' filter={inGroup(Sandbox)} {...Sandbox} /> - </Sidebars.SideBar> + </> ); } diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml index 207b2a4271edc18c074a4072e3e54eb752364fbb..7a425c05b53a61284af693ecbe7fe3f595e44ab0 100644 --- a/src/kernel_services/plugin_entry_points/log.ml +++ b/src/kernel_services/plugin_entry_points/log.ml @@ -562,11 +562,6 @@ let deferred_exn = ref DNo_exn let unreported_error = "##unreported-error##" -let unreported_event { evt_category } = - match evt_category with - | None -> false - | Some s -> s = unreported_error - (* we keep track of at most one deferred exception, ordered by seriousness (internal error > user error > warning-as-error). the rationale is that an internal error might cause subsequent errors or warning, but the reverse @@ -585,16 +580,20 @@ let update_deferred_exn exn = let warn_event_as_error event = update_deferred_exn (DWarn_as_error event) -let deferred_raise ~fatal ~unreported event msg = +let deferred_raise ~fatal event msg = (* reset deferred flag. *) let () = deferred_exn := DNo_exn in let channel = new_channel event.evt_plugin in - let append = - if unreported then None else - Some - (fun fmt -> - Format.fprintf fmt " See above messages for more information.@\n") + let pp_pos fmt pos = + if Filepath.is_empty_pos pos + then Format.fprintf fmt "<unknown location> " + else Format.fprintf fmt "%a: " Filepath.pp_pos pos + in + let pp_pos_opt = Pretty_utils.pp_opt pp_pos in + let print_event fmt = + Format.fprintf fmt "@\n%a%s" pp_pos_opt event.evt_source event.evt_message in + let append = Some print_event in let exn = if fatal then AbortFatal event.evt_plugin else AbortError event.evt_plugin @@ -606,23 +605,20 @@ let treat_deferred_error () = match !deferred_exn with | DNo_exn -> () | DWarn_as_error event -> - let unreported = unreported_event event in let wkey = match event.evt_category with | None -> "" | Some s when s = unreported_error -> "" | Some s -> s in - deferred_raise ~fatal:false ~unreported event - "warning %s treated as deferred error." wkey + deferred_raise ~fatal:false event + "warning %s treated as deferred error:" wkey | DError event -> - let unreported = unreported_event event in - deferred_raise ~fatal:false ~unreported event - "Deferred error message was emitted during execution." + deferred_raise ~fatal:false event + "Deferred error message was emitted during execution:" | DFatal event -> - let unreported = unreported_event event in - deferred_raise ~fatal:true ~unreported event - "Deferred internal error message was emitted during execution." + deferred_raise ~fatal:true event + "Deferred internal error message was emitted during execution:" (* -------------------------------------------------------------------------- *) (* --- Messages Interface --- *) diff --git a/src/plugins/wp/tests/wp/oracle/main_called.res.oracle b/src/plugins/wp/tests/wp/oracle/main_called.res.oracle index abd81c8221875403a618a45bd81066104ceb1186..91be9fd49b8b4a52be4c34885f19ad1c98baa4e0 100644 --- a/src/plugins/wp/tests/wp/oracle/main_called.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/main_called.res.oracle @@ -6,5 +6,7 @@ This case is not supported yet (skipped verification). [wp] Warning: No goal generated [wp] No proof obligations -[wp] User Error: Deferred error message was emitted during execution. See above messages for more information. +[wp] User Error: Deferred error message was emitted during execution: + Main entry point function 'main' is (potentially) recursive. + This case is not supported yet (skipped verification). [kernel] Plug-in wp aborted: invalid user input. diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle index 631d75f827d420ae2c29786b4c8fc31f18750369..64bcfd672f31e0790ded2c1f41579b14b29983d2 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle @@ -16,5 +16,7 @@ Goal Instance of 'Pre-condition 'qed_ok,Rmain' in 'main'' in 'call_main' at call Prove: true. ------------------------------------------------------------ -[wp] User Error: Deferred error message was emitted during execution. See above messages for more information. +[wp] User Error: Deferred error message was emitted during execution: + Main entry point function 'main' is (potentially) recursive. + This case is not supported yet (skipped verification). [kernel] Plug-in wp aborted: invalid user input. diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle index d9d2494634c67b2e7ba783f6f935dd48f757c76c..36cc360ff042bfb0637d89b099a79d072c2fa9ed 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.1.res.oracle @@ -8,5 +8,7 @@ [wp] User Error: Main entry point function 'main' is (potentially) recursive. This case is not supported yet (skipped verification). [wp] No proof obligations -[wp] User Error: Deferred error message was emitted during execution. See above messages for more information. +[wp] User Error: Deferred error message was emitted during execution: + Main entry point function 'main' is (potentially) recursive. + This case is not supported yet (skipped verification). [kernel] Plug-in wp aborted: invalid user input. diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle index 77cbd8d8902446fa20846f04d51e990a5230d8dc..d726ead78f0c65a68882bd8bf9c8ba3f0d996547 100644 --- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle +++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle @@ -22,5 +22,7 @@ Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initiali Prove: true. ------------------------------------------------------------ -[wp] User Error: Deferred error message was emitted during execution. See above messages for more information. +[wp] User Error: Deferred error message was emitted during execution: + Main entry point function 'main' is (potentially) recursive. + This case is not supported yet (skipped verification). [kernel] Plug-in wp aborted: invalid user input. diff --git a/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle index d5852e56a1789c285c609b16d212a2cf833ced2d..7626e418a06b742861746c2e5bb1a7fc6015267c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/import_unexisting.res.oracle @@ -3,5 +3,6 @@ [wp] User Error: Library Module not found [wp] Running WP plugin... [wp] No proof obligations -[wp] User Error: Deferred error message was emitted during execution. See above messages for more information. +[wp] User Error: Deferred error message was emitted during execution: + Library Module not found [kernel] Plug-in wp aborted: invalid user input. diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle index f3b4277224c93fb69cbb10608120722ec1f105cf..8fd6e6a5253fd99e84d2b57ab877c21d74f1345a 100644 --- a/tests/cil/oracle/ghost_cfg.0.res.oracle +++ b/tests/cil/oracle/ghost_cfg.0.res.oracle @@ -37,5 +37,7 @@ /*@ ghost goto X; */ [kernel:ghost:bad-use] ghost_cfg.c:109: Warning: '__retres' is a non-ghost lvalue, it cannot be assigned in ghost code -[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information. +[kernel] Warning: warning ghost:bad-use treated as deferred error: + ghost_cfg.c:10: Ghost code breaks CFG starting at: + /*@ ghost goto X; */ [kernel] Frama-C aborted: invalid user input. diff --git a/tests/cil/oracle/ghost_cfg.1.res.oracle b/tests/cil/oracle/ghost_cfg.1.res.oracle index b57f33e7f5f5c58944585e439afcaaf45c51dd11..0448e9490f95a39d2f4e8589fec8a3bf606af5ab 100644 --- a/tests/cil/oracle/ghost_cfg.1.res.oracle +++ b/tests/cil/oracle/ghost_cfg.1.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing ghost_cfg.c (with preprocessing) [kernel] ghost_cfg.c:154: User Error: 'goto X;' would jump from normal statement to ghost code -[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information. +[kernel] User Error: Deferred error message was emitted during execution: + ghost_cfg.c:154: 'goto X;' would jump from normal statement to ghost code [kernel] Frama-C aborted: invalid user input. diff --git a/tests/misc/oracle/debug_category.14.res.oracle b/tests/misc/oracle/debug_category.14.res.oracle index f7d982e9f13f7f2910553db3af0c8978c792bb6c..a23f0ff8463c73970509e3446bc5942f650fb4a6 100644 --- a/tests/misc/oracle/debug_category.14.res.oracle +++ b/tests/misc/oracle/debug_category.14.res.oracle @@ -3,5 +3,7 @@ [test:a] Warning: Warning A (warn-error-once: no further messages from category 'a' will be emitted) -[test] Warning: warning a treated as deferred error. See above messages for more information. +[test] Warning: warning a treated as deferred error: + Warning A + (warn-error-once: no further messages from category 'a' will be emitted) [kernel] Plug-in test aborted: invalid user input. diff --git a/tests/misc/oracle/debug_category.15.res.oracle b/tests/misc/oracle/debug_category.15.res.oracle index b33ecc559a42c3b34bcbacc30b92a4fa569cf051..24eb2787f227400b3417a6c89d639eedaabc4be6 100644 --- a/tests/misc/oracle/debug_category.15.res.oracle +++ b/tests/misc/oracle/debug_category.15.res.oracle @@ -3,5 +3,6 @@ [test:a] Warning: Warning A [test] User Error: Testing error function [test:a] Warning: Another Warning A -[test] User Error: Deferred error message was emitted during execution. See above messages for more information. +[test] User Error: Deferred error message was emitted during execution: + Testing error function [kernel] Plug-in test aborted: invalid user input. diff --git a/tests/misc/oracle/debug_category.16.res.oracle b/tests/misc/oracle/debug_category.16.res.oracle index 6857c762cdb581b0e618826742415ce950b0b6b1..05ddb3b964e48824c4d98ad919e9c47506211d8d 100644 --- a/tests/misc/oracle/debug_category.16.res.oracle +++ b/tests/misc/oracle/debug_category.16.res.oracle @@ -2,5 +2,6 @@ [test] Warning: Uncategorized warning [test:a] Warning: Warning A [test:a] Warning: Another Warning A -[test] Failure: Deferred error message was emitted during execution. +[test] Failure: Deferred error message was emitted during execution: + Silent error [kernel] Plug-in test aborted: invalid user input. diff --git a/tests/misc/oracle/debug_category.17.res.oracle b/tests/misc/oracle/debug_category.17.res.oracle index 64448bd5bd4427d7ac9cf9d550df0bb57d79048c..9175eca5cbcb173c0d9b7180c85dc5affc38b916 100644 --- a/tests/misc/oracle/debug_category.17.res.oracle +++ b/tests/misc/oracle/debug_category.17.res.oracle @@ -3,7 +3,8 @@ [test:a] Warning: Warning A [test] Failure: Testing failure function [test:a] Warning: Another Warning A -[test] Failure: Deferred internal error message was emitted during execution. See above messages for more information. +[test] Failure: Deferred internal error message was emitted during execution: + Testing failure function [kernel] Current source was: <unknown> The full backtrace is: diff --git a/tests/misc/oracle/debug_category.8.res.oracle b/tests/misc/oracle/debug_category.8.res.oracle index 66200a611dba982af8261ffa538670a8f3908d45..ce16a8ff180d532472446d3b43e1f9b51bc13d68 100644 --- a/tests/misc/oracle/debug_category.8.res.oracle +++ b/tests/misc/oracle/debug_category.8.res.oracle @@ -2,5 +2,6 @@ [test] Warning: Uncategorized warning [test:a] Warning: Warning A [test:a] Warning: Another Warning A -[test] Warning: warning a treated as deferred error. See above messages for more information. +[test] Warning: warning a treated as deferred error: + Warning A [kernel] Plug-in test aborted: invalid user input. diff --git a/tests/spec/oracle/Extend_errors.3.res.oracle b/tests/spec/oracle/Extend_errors.3.res.oracle index c12d7dc67efde446c9feaab6790b0eebbe0c0ffe..f893faa813a57608b9a338cdec352fbe977a1cb7 100644 --- a/tests/spec/oracle/Extend_errors.3.res.oracle +++ b/tests/spec/oracle/Extend_errors.3.res.oracle @@ -4,5 +4,6 @@ Ignoring unregistered extension 'bar' of plug-in myplugin1 [kernel:plugin-not-loaded] Extend_errors.c:33: Warning: Ignoring extension 'bar' for unloaded plug-in unknown_plugin -[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information. +[kernel] Warning: warning extension-unknown treated as deferred error: + Extend_errors.c:32: Ignoring unregistered extension 'bar' of plug-in myplugin1 [kernel] Frama-C aborted: invalid user input. diff --git a/tests/spec/oracle/import_errors.2.res.oracle b/tests/spec/oracle/import_errors.2.res.oracle index 67fa872774041b03672abbc5648fda68da0896f8..aafb590e9481c94e3cba683e957d69bd23edfa40 100644 --- a/tests/spec/oracle/import_errors.2.res.oracle +++ b/tests/spec/oracle/import_errors.2.res.oracle @@ -2,5 +2,6 @@ [kernel] Parsing import_errors.c (with preprocessing) [kernel:extension-unknown] import_errors.c:40: Warning: Ignoring unregistered module importer extension 'toto' of plug-in myplugin1 -[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information. +[kernel] Warning: warning extension-unknown treated as deferred error: + import_errors.c:40: Ignoring unregistered module importer extension 'toto' of plug-in myplugin1 [kernel] Frama-C aborted: invalid user input. diff --git a/tests/spec/oracle/import_errors.3.res.oracle b/tests/spec/oracle/import_errors.3.res.oracle index fba570a595ecc22384efbab28e1cb41a2cc58d5a..59d145fb2faaf23fad0dee78b7f3ede5d3ddad6a 100644 --- a/tests/spec/oracle/import_errors.3.res.oracle +++ b/tests/spec/oracle/import_errors.3.res.oracle @@ -2,5 +2,6 @@ [kernel] Parsing import_errors.c (with preprocessing) [kernel:extension-unknown] import_errors.c:44: Warning: Ignoring unregistered module importer extension 'toto' -[kernel] Warning: warning extension-unknown treated as deferred error. See above messages for more information. +[kernel] Warning: warning extension-unknown treated as deferred error: + import_errors.c:44: Ignoring unregistered module importer extension 'toto' [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/cert_msc_38.1.res.oracle b/tests/syntax/oracle/cert_msc_38.1.res.oracle index 2f08c1db2a30eaf2d8c55dbf6f5afad12a153c21..3f1bf2f4589d1b851a2668f3dd22a9004d3a54c9 100644 --- a/tests/syntax/oracle/cert_msc_38.1.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.1.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing cert_msc_38.c (with preprocessing) [kernel:CERT:MSC:38] cert_msc_38.c:33: Warning: Attempt to declare errno as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C -[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information. +[kernel] Warning: warning CERT:MSC:38 treated as deferred error: + cert_msc_38.c:33: Attempt to declare errno as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/cert_msc_38.2.res.oracle b/tests/syntax/oracle/cert_msc_38.2.res.oracle index fe19cf1bb736df3777123bdfcf4b2f939dc4d1af..6d067c08966d150faf7ccafdb693d2e4e3ef9d8b 100644 --- a/tests/syntax/oracle/cert_msc_38.2.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.2.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing cert_msc_38.c (with preprocessing) [kernel:CERT:MSC:38] cert_msc_38.c:38: Warning: Attempt to declare math_errhandling as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C -[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information. +[kernel] Warning: warning CERT:MSC:38 treated as deferred error: + cert_msc_38.c:38: Attempt to declare math_errhandling as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/cert_msc_38.7.res.oracle b/tests/syntax/oracle/cert_msc_38.7.res.oracle index e4f28025579f70f1ac20a1113b04fc604ce3d881..21c18c167b7bb1e92d9fa0f5e9aca9bddd2426df 100644 --- a/tests/syntax/oracle/cert_msc_38.7.res.oracle +++ b/tests/syntax/oracle/cert_msc_38.7.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing cert_msc_38.c (with preprocessing) [kernel:CERT:MSC:38] cert_msc_38.c:60: Warning: setjmp is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C -[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information. +[kernel] Warning: warning CERT:MSC:38 treated as deferred error: + cert_msc_38.c:60: setjmp is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/ghost_cv_incompat.res.oracle b/tests/syntax/oracle/ghost_cv_incompat.res.oracle index 2e709e806388d3d2de3d29704a72a1f3579083b9..67144a2682d9c7de445d5d2ff41ee4666be77beb 100644 --- a/tests/syntax/oracle/ghost_cv_incompat.res.oracle +++ b/tests/syntax/oracle/ghost_cv_incompat.res.oracle @@ -93,5 +93,6 @@ Invalid cast of '& g_0' from 'int \ghost *' to 'int *' [kernel:ghost:bad-use] ghost_cv_incompat.i:194: Warning: Invalid cast of '& g_0' from 'int \ghost *' to 'int *' -[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information. +[kernel] Warning: warning ghost:bad-use treated as deferred error: + ghost_cv_incompat.i:27: Invalid cast of '& ng' from 'int *' to 'int \ghost *' [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle index daaa1f8c77466c6e7bc074e39cac24b2e864f0e7..4d5eba0305e79dba044063a0c51eba6fae1eb822 100644 --- a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle +++ b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle @@ -57,5 +57,6 @@ Call to non-ghost function from ghost code is not allowed [kernel:ghost:bad-use] ghost_cv_invalid_use.i:162: Warning: Call to non-ghost function from ghost code is not allowed -[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information. +[kernel] Warning: warning ghost:bad-use treated as deferred error: + ghost_cv_invalid_use.i:14: 'ng' is a non-ghost lvalue, it cannot be assigned in ghost code [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle b/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle index 5a8bba7de39ff6df5c6fd0f648ddc17b38692e7e..1c84f13933e32e0c2c2a7db91ce5f5019c569252 100644 --- a/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle +++ b/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle @@ -27,5 +27,6 @@ Invalid type for 'param': indirection from non-ghost to ghost [kernel:ghost:bad-use] ghost_cv_var_decl.c:166: Warning: Invalid type for 'pptrg': indirection from non-ghost to ghost -[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information. +[kernel] Warning: warning ghost:bad-use treated as deferred error: + ghost_cv_var_decl.c:152: No definition, nor assigns specification for ghost function 'decl_bad_return_type' [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/too_large_array.res.oracle b/tests/syntax/oracle/too_large_array.res.oracle index c5df2b706f22b915013c35ed485c5bfbcc44301b..0e7bd1d67b305b692466a812cf057694fadce13a 100644 --- a/tests/syntax/oracle/too_large_array.res.oracle +++ b/tests/syntax/oracle/too_large_array.res.oracle @@ -3,5 +3,6 @@ Array length is too large. [kernel] too_large_array.i:12: Warning: Cannot represent length of array as an attribute -[kernel] Warning: warning too-large-array treated as deferred error. See above messages for more information. +[kernel] Warning: warning too-large-array treated as deferred error: + too_large_array.i:12: Array length is too large. [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle index 3270a28dd6f5ba3e83b7c88e4fb0e848db680b77..c539276b5271aff91e9c791fb3410fdda8c0d1d1 100644 --- a/tests/syntax/oracle/very_large_integers.11.res.oracle +++ b/tests/syntax/oracle/very_large_integers.11.res.oracle @@ -29,5 +29,6 @@ ---------------------------------------------------------------------------- No logical properties have been reached by the analysis. ---------------------------------------------------------------------------- -[kernel] Warning: warning annot-error treated as deferred error. See above messages for more information. +[kernel] Warning: warning annot-error treated as deferred error: + very_large_integers.c:132: Invalid slevel directive. Ignoring code annotation [kernel] Frama-C aborted: invalid user input. diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle index 7c23fb2f46bdc345a531f6c51dd40c56e694ed4a..77c360b499a70035566cfb11d6a7deacfac6ff26 100644 --- a/tests/value/oracle/recursion.2.res.oracle +++ b/tests/value/oracle/recursion.2.res.oracle @@ -50,5 +50,8 @@ Frama_C_entropy_source; x; y; tmp; tmp_0; tmp_1 [inout] Inputs for function main_fail: Frama_C_entropy_source -[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information. +[eva] Warning: warning assigns:missing treated as deferred error: + recursion.c:426: Recursive call to sum_nospec without assigns clause. + Generating probably incomplete assigns to interpret the call. + Try to increase the -eva-unroll-recursive-calls parameter or write a correct specification for function sum_nospec. [kernel] Plug-in eva aborted: invalid user input. diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle index 942c944e4ecaa136ff3b103a4c2a9a2fa22292fb..a82c098f3a1124a585a91636c24fa3a48cf56f27 100644 --- a/tests/value/oracle/use_spec.0.res.oracle +++ b/tests/value/oracle/use_spec.0.res.oracle @@ -74,5 +74,6 @@ x; y Sure outputs: w; z -[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information. +[eva] Warning: warning assigns:missing treated as deferred error: + No assigns specified for function 'f' for which option -eva-use-spec is set. Generating potentially incorrect assigns. [kernel] Plug-in eva aborted: invalid user input. diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle index ceeb03a639742555ef684cd431159b8abe3c0bc6..f3e0269226cc04e147a796139fb2146cf7540aa0 100644 --- a/tests/value/oracle/use_spec.1.res.oracle +++ b/tests/value/oracle/use_spec.1.res.oracle @@ -74,5 +74,6 @@ x; y Sure outputs: w; z -[eva] Warning: warning assigns:missing treated as deferred error. See above messages for more information. +[eva] Warning: warning assigns:missing treated as deferred error: + No assigns specified for function 'f' for which option -eva-use-spec is set. Generating potentially incorrect assigns. [kernel] Plug-in eva aborted: invalid user input. diff --git a/tests/value/oracle/va_list.1.res.oracle b/tests/value/oracle/va_list.1.res.oracle index 3e0140e510878b7c47e20684214c596823298e18..2a493c5ef3c670e835f1b9dc2f66b01ff52db8fb 100644 --- a/tests/value/oracle/va_list.1.res.oracle +++ b/tests/value/oracle/va_list.1.res.oracle @@ -30,5 +30,6 @@ vlParameters; tmp [inout] Inputs for function main: \nothing -[eva] User Error: Deferred error message was emitted during execution. See above messages for more information. +[eva] User Error: Deferred error message was emitted during execution: + va_list.c:14: functions returning variadic arguments must be stubbed [kernel] Plug-in eva aborted: invalid user input.