| Ref
| Details
| Workaround
| Action planned
|
| 70
| If a searchrule is interrupted (Interactive Prover), then the previous interactive command is suppressed.
|
| Correction in Atelier B 4.1
|
| 73
| Apparition of zombie processes sometimes (submitted by Siemens Transportation Systems)
|
| Correction in Atelier B 4.1
|
| 203
| When several Typechecks are performed simultaneously, some component statuses may be lost.
|
| Correction in Atelier B 4.1
|
| 208
| Cross-referencer should be able to generate operation call graph
|
| Correction in Atelier B 4.1
|
| 260
| The Predicate Prover produces typecheck errors when using prj2 operator.
|
| Corrected in Atelier B 4.0.1
|
| 261
| Typechecker and B Compiler analyze differently a substitution containing an erroneous operation call, on a particular example. One tool accepts the subsitution while the other rejects it.
|
| Correction in Atelier B 4.1
|
| 264
| Several hours for generating proof obligations, for a particular example provided by Siemens Transportation Systems.
|
| Correction in Atelier B 4.0.2
|
| 272
| Generation of proof obligations fails for a particular project, provided by David Deharbe.
|
| Correction in Atelier B 4.1
|
| 321
| When krt can't be started (in MsServ.C), quitting the program raises an assert:
Assertion failed: file != __null, file m_pmana.cpp, line 202
|
| Correction in Atelier B 4.1
|
| 334
| Choosing to display components with the hierarchical view is not memorized.
| Select "Hierarchical view" when opening a project.
| Correction in Atelier B 4.1
|
| 399
| Some atom constructors ( /: , /= , <= and >= ) have a priority 160, greater than some term operators (i.e. 125 for <-> ). Syntax analysis may produce absurd results (AA<->AA/=BB) is analysed as (AA <-> not(AA=BB) )
|
| Correction in Atelier B 4.1
|
| 452
| Incompatible bcomp file formats (from one version of Atelier B to another) may lead the bbatch to crash.
|
| Magic numbers will be modified in order to detect incompatible files.
Correction in Atelier B 4.1
|
| 465
| When a project is located in a directory with a name containing accents, bbatch is not able to open the project. A message is displayed in a QMessageBox: "Error Reading Bbatch output". WHen the bbatch has crashed, Atelier B is completely stucked.
|
| Corrected in Atelier B 4.0.1
|
| 466
| In the case of the following architecture, false reffinements may be proved:
- implementation C_i sees A and D
- machine D sees B
- implementation A_i implements A and imports B
It happens when D contains an operation reading a variable of B which is modified through A.
Architecture controls that happen during implementation translation have to be completed.
|
| Corrected in Atelier B 4.0.1
|
| 469
| When restoring a project under Windows, dates may be not well-formed (files being generated/updated before others have time stamps located after files generated/updated after). This is probably due to the windows ziplib conversion routines, as their time stamps are 64 bits long and precise up to 1ns.
|
| Correction in 4.1
|
| 494
| Components of seen libraries can't be opened through navigation
|
| Corrected in Atelier B 4.0.1
|
| 495
| Components accessed through navigation can't be navigated
|
| Corrected in Atelier B 4.0.1
|
| 496
| B Compiler crashes when using the refinement wizard to generate a refinement, in a particular case.
|
| Corrected in Atelier B 4.0.1
|
| 504
| A not typechecked refinement is not shown in the hierachical display mode (in the main window and in the worskpace window)
| Leaving the hierachical display mode makes the compoent to re-appear in both windows
| Correction in Atelier B 4.1
|
| 507
| In some cases, the workspace window displays project and component symbols, before they are effectively created, leading to erroneous representation in case of error preventing project or component creation.
|
| Correction in Atelier B 4.1
|
| 526
| Generation of an archive file for a project (models + proof files) may lead to a crash on MacOs
|
| Correction in Atelier B 4.1
|
| 532
| Incorrect line counter when using buffered commands
|
| Corrected in Atelier B 4.0.1
|
| 536
| Considering a machine containing 2 events e1 and e2. A refinement of this machine may define e1 as
e1 ref e2
which should not be allowed.
| Avoid to use this refinement schema
| Correction in Atelier B 4.1
|
| 549
| In interactive proof mode, when the proof tree contains too many nested commands, the horizontal scrollbar doesn't offer access to the right hand side commands.
|
| Correction in Atelier B 4.1
|
| 572
| In interactive proof mode, the command window may be unreachable if resizing it too small. That could be very disturbing for new users who don't know that this window exists.
|
| Correction in Atelier B 4.1
|
| 575
| Well-definedness proof obligations for ASSERT are duplicated
|
| Corrected in Atelier B 4.0.1
|
| 576
| When local variables (VAR .. IN .. END) are valued with a value inside a IF .. THEN .. ELSE .. END, or when they are typed by a "becomes such that" substitution, erroneous well-definedness proof obligations are generated (submitted by Siemens Transportation Systems)
|
| Corrected in Atelier B 4.0.1
|
| 579
| For a distributed project (paralelizer), in case of a ssh connection problem or if the B project doesn't exist on the remote computer, no error message is displayed. The task keeps the "wait" status foerever.
|
| Correction in Atelier B 4.1
|
| 580
| With a distributed project (paralelizer), errors displayed in the error window are not related to the computer where they happened (no location information is displayed).
|
| Correction in Atelier B 4.1
|
| 581
| When replaying a project over a set of distributed computers (paralelizer), error pop-ups show up, without any information about the computer where they are related to, and no information is displayed in the error window.
|
| Correction in Atelier B 4.1
|
| 588
| Atelier B 4.0 GUI crashes at startup on Solaris workstations, due to incompatible libraries (submitted by Siemens Transportation Systems)
|
| Corrected in Atelier B 4.0.1
|
| 604
| Errors in the French Language package (submitted and corrected by David Deharbe)
|
| Corrected in Atelier B 4.0.1
|
| 606
| No visual information of what kind of prover (force 0, force 1, user pass, etc.) has been used on a given component.
|
| Correction in Atelier B 4.1
|
| 607
| B0check errors were underlined in red, which could be perturbating for users not willing to generate code (and as such not willing to comply with B0 restrictions).
|
| Corrected in Atelier B 4.0.1
|
| 608
| Proof obligations generator is not merging existing obvious proof obligations with new ones
|
| Corrected in Atelier B 4.0.1
|
| 609
| Some proof obligations, related to post-conditions verification, are not generated (in relation with the type of local operations output parameters)
|
| Corrected in Atelier B 4.0.1
|
| 610
| When a machine produces obvious proof obligations (.opo file) but no proof obligations, the .opo file is syntaxically incorrect.
|
| Corrected in Atelier B 4.0.1
|
| 611
| In interactive proof mode, when using pr command in trace mode, messages indicating which rules are applied are not displayed.
|
| Correction in Atelier B 4.1
|
| 612
| Interactive prover crash when proving machines containing enumerated sets (linux)
| The following workaround can be used
| Corrected in Atelier B 4.0.1
|
| 615
| FIN and FIN1 are not colorized in the interactive prover.
|
| Corrected in Atelier B 4.0.1
|
| 617
| Messages in search windows (hypothesis, rule) and main prover window can't be flushed
|
| Correction in Atelier B 4.1
|
| 618
| The editor doesn't allow to "Go to" a line greater than 99
| Scroll manually
| Correction in Atelier B 4.1
|
| 620
| With the wizard enabling to generate a new refinement from a model, substitutions like
{xx | P}
seem to be copied as
{xx xx | P}
leading to typecheck error.
| Correct the generated model manually.
| Corrected in Atelier B 4.0.1
|
| 622
| When long error messages are displayed, horizontal scrolling the window is mandatory and text is difficult to read.
|
| Option offered to display text over several lines
Correction in Atelier B 4.1
|
| 623
| BTAGS crashes on Mac for a given B model (provided by David Kelk)
|
| Corrected in Atelier B 4.0.1
|
| 630
| Feasability proof obligations, for some kinds of events, are incorrect in the refinement.
|
| Corrected in Atelier B 4.0.1
|
| 650
| Copying a demonstration from within the interactive prover may lead to a crash, when right-clicking one of the triangles appearing in the proof tree and selecting "copy" menu item.
| The copy fails and leads to a crash if no command is selected. Click on any command of the proof tree before copying.
| Corrected in Atelier B 4.0.1
|
| 653
| Following information are missing in the project status:
- distinction between automatic and interactive proofs,
- number of user rules,
- number of lines of B
|
| Correction in Atelier B 4.1
|
| 657
| Refinement wizard (component creation) doesn't handle a, b := c, d correctly
| Transform your substitution into a := c ; b := d
| Corrected in Atelier B 4.0.1
|
| 675
| Event-based refinement with .sys for the GUi and with .ref for the bcomp
| Atelier B creates event-based refinements with .sys files, bcomp with .ref files. Semantic analysis faisl when initiated with a .sys refinement.
| Correction in Atelier B 4.1
|
| Ref
| Details
| Workaround
| Action planned
|
| 318
| The guard bsubfrm is missing in the rule language
|
| Correction in Atelier B 4.1
|
| 566
| Bart can't refine machines containing SETS or CONSTANTS. However, no error message is displayed.
| SETS and CONSTANTS have to be defined in separate machines (context machines)
| Correction in Atelier B 4.1
|
| 645
| When a rule file (rmf) is reloaded in the GUI after a modification, errors are displayed (pop-up) but not the warnings.
|
| Correction in Bart 1.1
|
| 647
| When argument -t is used, Bart doesn't print out the name of the rules used to refine substitutions.
|
| Correction in Bart 1.1
|
| 648
| Proof work is not reused by the proof obligation generator / merger, when executing an automatic refinement, meaning that interactive demonstration are lost.
| Interactive demonstrations have to be saved in the User_Pass theory in Pmm file. Demonstrations can then be replayed (menu Proof-> User Pass).
| Correction in Atelier B 4.1
|
| 649
| Bart may enter an infinite loop when applying a looping rule. Bart executable grows til occupying all memory, leading the computer to swap, until no more resources are available.
|
| introduction of a timer or rule application counter
Correction in Atelier B 4.1
|
| 651
| B file headers, generated by BART, are incorrect (see date field):
/* block_occupancy_3_i
* This file has been generated by BART (B Automatic Refinement Tool)
* Generated the ATION4/2009
* DO NOT EDIT */
|
| Correction in Atelier B 4.1
|
| 655
| Rules assign_a_union_b_c_1 and assign_a_minus_b_c_5 are not correct (parentheses are missing in the invariant)
| In rule assign_a_union_b_c_1, invariant should be:
invariant => (@a = @a$0 \/ (@c_traites /\ (@b))))
in rule assign_a_minus_b_c_5, invariant should be:
invariant => (@a = @a$0 - (@c_traites /\ (@b))))
| Correction in Atelier B 4.1
|
| 656
| Components generated by Bart, once suppressed by user interaction, still remain when switching to hierachical view.
| Closing/opening the project solves the problem.
| Correction in Atelier B 4.1
|
| 658
| pragma EMPRILE_PRE is not working properly
|
| Correction in Atelier B 4.1
|